-
Notifications
You must be signed in to change notification settings - Fork 134
Pull requests: leanprover-community/physlib
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat(ClassicalMechanics): add rigid-body angular momentum and prove L = Iω
awaiting-author
A reviewer has asked the author a question or requested changes
#1366
opened Jul 4, 2026 by
giuseppesorge
Contributor
Loading…
feat(Thermodynamics): add foundational API
awaiting-author
A reviewer has asked the author a question or requested changes
RFC
Request for comment
t-thermodynamics
Thermodynamics
#1365
opened Jul 4, 2026 by
nateabr
Contributor
Loading…
auto-task(positionOperatorSchwartz): fix doc-string mislabeling it the parity operator
#1362
opened Jul 3, 2026 by
jstoobysmith
Member
Loading…
feat: Add equivariance to ConjTensorSpecies
#1358
opened Jul 2, 2026 by
jstoobysmith
Member
Loading…
feat(PhyslibAlpha/Particles): The effective potential of the 2HDM
PhyslibAlpha
Pull requests which are for modifications to PhyslibAlpha.
#1357
opened Jul 2, 2026 by
jstoobysmith
Member
Loading…
feat: report golf compile cost (heartbeats + time) in /check-golf
#1356
opened Jul 2, 2026 by
Vilin97
Contributor
Loading…
feat: add /check-golf bot verifying statements are unchanged
#1355
opened Jul 2, 2026 by
Vilin97
Contributor
Loading…
auto-task(exists_boost_mul_rotation): prove restricted Lorentz elements are a boost times a rotation
#1350
opened Jul 1, 2026 by
jstoobysmith
Member
Loading…
refactor: Rising and lowering indices with notation
t-relativity
Relativity
#1348
opened Jul 1, 2026 by
jstoobysmith
Member
Loading…
feat: Add DropPair ProdP commutation lemma for one orientation
awaiting-author
A reviewer has asked the author a question or requested changes
#1345
opened Jul 1, 2026 by
NicolaBernini
Contributor
Loading…
feat(Relativity): epsilon-epsilon contraction identities for the Levi-Civita tensor
awaiting-author
A reviewer has asked the author a question or requested changes
#1335
opened Jun 30, 2026 by
Robby955
Contributor
Loading…
feat: Close the smallest pendulum configuration-space sorryful definitions
awaiting-author
A reviewer has asked the author a question or requested changes
#1327
opened Jun 30, 2026 by
NicolaBernini
Contributor
Loading…
auto-task(EffectivePotential): TODO to make Higgs potential polynomial basis-independent
awaiting-author
A reviewer has asked the author a question or requested changes
#1321
opened Jun 29, 2026 by
jstoobysmith
Member
Loading…
auto-task(Fermion.dirac): record TODO to add Dirac fermion representations and Color
#1317
opened Jun 29, 2026 by
jstoobysmith
Member
Loading…
feat: Refactor downstream use away from FieldStrengthMatrix
awaiting-author
A reviewer has asked the author a question or requested changes
#1288
opened Jun 26, 2026 by
NicolaBernini
Contributor
Loading…
refactor: Add Contractions in terms of representations
t-relativity
Relativity
#1253
opened Jun 24, 2026 by
jstoobysmith
Member
Loading…
chore(QuantumInfo): clear 56 files from the linter exemption list
#1244
opened Jun 24, 2026 by
tracyphasespace
Contributor
Loading…
feat: gamma anticommutator and slash of Lorentz vector
awaiting-author
A reviewer has asked the author a question or requested changes
#1206
opened Jun 18, 2026 by
wdconinc
Contributor
Loading…
feat(QuantumInfo): angle-parameterized qubit ket for Pancharatnam connection
awaiting-author
A reviewer has asked the author a question or requested changes
#1139
opened Jun 2, 2026 by
wock9000
Contributor
Loading…
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.