Skip to content

Actions: leanprover-community/physlib

Actions

PR Comment

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
PRMessage.yml
204 workflow runs
204 workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
feat(QuantumMechanics): Add TODOs PR Comment #204: Pull request #1359 opened by gloges
29s
29s
feat: Add equivariance to ConjTensorSpecies PR Comment #203: Pull request #1358 opened by jstoobysmith
32s
32s
feat(PhyslibAlpha/Particles): The effective potential of the 2HDM PR Comment #202: Pull request #1357 opened by jstoobysmith
26s
26s
feat: report golf compile cost (heartbeats + time) in /check-golf PR Comment #201: Pull request #1356 opened by Vilin97
31s
31s
feat: add /check-golf bot verifying statements are unchanged PR Comment #200: Pull request #1355 opened by Vilin97
36s
36s
feat(ClassicalMechanics): add Caldirola-Kanai lagrangian for the damped harmonic oscillator PR Comment #199: Pull request #1354 opened by giuseppesorge
30s
30s
feat(ClassicalMechanics): add rigid-body angular velocity tensor PR Comment #198: Pull request #1353 opened by giuseppesorge
29s
29s
Add Euler-Lagrange equation API to PhyslibAlpha PR Comment #197: Pull request #1352 opened by juanjfndz
26s
26s
Add extensionality for finite-measure distributions PR Comment #196: Pull request #1351 opened by Lemmy00
30s
30s
auto-task(exists_boost_mul_rotation): prove restricted Lorentz elements are a boost times a rotation PR Comment #195: Pull request #1350 opened by jstoobysmith
28s
28s
auto-task(PlaneSeven.B): remove B₀–B₆ definitions in favour of a single B : Fin 7 → Charges PR Comment #194: Pull request #1349 opened by jstoobysmith
31s
31s
refactor: Rising and lowering indices with notation PR Comment #193: Pull request #1348 opened by jstoobysmith
25s
25s
Bridge Physlib distributions to tempered distributions PR Comment #192: Pull request #1347 opened by Lemmy00
35s
35s
feat: Document succSuccAbove implementation tradeoff PR Comment #191: Pull request #1346 opened by NicolaBernini
34s
34s
feat: Add DropPair ProdP commutation lemma for one orientation PR Comment #190: Pull request #1345 opened by NicolaBernini
29s
29s
feat: Add first EvalT and ProdT Interaction Lemma PR Comment #189: Pull request #1344 opened by NicolaBernini
27s
27s
feat: Add the first EvaltT/PermT Interaction Lemma PR Comment #188: Pull request #1343 opened by NicolaBernini
31s
31s
auto-task(TwoHDM): add API-map.yaml tracking the Two Higgs Doublet Model API PR Comment #187: Pull request #1342 opened by ShlokVaibhav
31s
31s
auto-task(Space): add API-map.yaml tracking the Space API PR Comment #186: Pull request #1341 opened by ShlokVaibhav
26s
26s
auto-task(HarmonicOscillator): add API-map.yaml tracking the Harmonic oscillator API PR Comment #185: Pull request #1340 opened by ShlokVaibhav
27s
27s
auto-task(RigidBody): add API-map.yaml tracking the Rigid body API PR Comment #184: Pull request #1339 opened by ShlokVaibhav
25s
25s
refactor(QuantumMechanics): SpaceDHilbertSpace API PR Comment #183: Pull request #1338 opened by gloges
30s
30s
feat(LorentzGroup): realize as a closed subgroup of GL PR Comment #182: Pull request #1337 opened by Robby955
28s
28s
refactor(Tensors): remove pre-Lorentz Contr/Co reps in favour of ContrMod.rep/CoMod.rep PR Comment #181: Pull request #1336 opened by Robby955
32s
32s
feat(Relativity): epsilon-epsilon contraction identities for the Levi-Civita tensor PR Comment #180: Pull request #1335 opened by Robby955
28s
28s