-
Notifications
You must be signed in to change notification settings - Fork 102
Pull requests: leanprover-community/physlib
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat(SpaceAndTime): first-step GalileanGroup API (data type and coordinate action)
#1116
opened May 21, 2026 by
MaxwellLaw
Loading…
5 tasks done
feat(QM): Add Quantum mechanics
SpaceDQuantumSystem
t-quantum-mechanics
#1114
opened May 21, 2026 by
gloges
Contributor
Loading…
feat(SUSY/N1): add chiral scalar configuration space and coordinate CLMs
#1113
opened May 20, 2026 by
pariandrea
Loading…
feat(FluidDynamics): add Navier-Stokes conservative and convective forms
#1112
opened May 20, 2026 by
FloWsnr
Contributor
Loading…
feat(QuantumMechanics): sudden frequency change for the QHO
#1109
opened May 19, 2026 by
casualPhysics
Collaborator
Loading…
6 tasks done
feat: Wirtinger calculus and N=1 SUSY scalar Wirtinger derivatives
#1107
opened May 18, 2026 by
pariandrea
Loading…
refactor: Rename dropPairEmb to Fin.succSuccAbove
RFC
Request for comment
#1099
opened May 14, 2026 by
jstoobysmith
Member
Loading…
feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap
#1098
opened May 13, 2026 by
dennj
Contributor
Loading…
feat(Tensors): PermCond.snoc PermCond.succAbove
#1097
opened May 13, 2026 by
jstoobysmith
Member
Loading…
feat(QuantumMechanics): add Canonical commutation on the Schwartz submodule
t-quantum-mechanics
Quantum mechanics
#1096
opened May 13, 2026 by
or4nge19
Collaborator
Loading…
feat(QuantumMechanics): Uncertainty bounds for partial linear maps
t-quantum-mechanics
Quantum mechanics
#1095
opened May 13, 2026 by
or4nge19
Collaborator
Loading…
feat(Entropy): prove sandwiched Rényi DPI; remove axiom
awaiting-author
A reviewer has asked the author a question or requested changes
#1073
opened May 2, 2026 by
dennj
Contributor
Loading…
feat: Start split of Distributional EM
RFC
Request for comment
t-electromagnetism
Electromagnetism
#1063
opened Apr 28, 2026 by
jstoobysmith
Member
Loading…
refactor: Separate Vector.Basic & CoVector.Basic
RFC
Request for comment
t-relativity
Relativity
#1050
opened Apr 21, 2026 by
jstoobysmith
Member
Loading…
Add bounded derivative indices
awaiting-author
A reviewer has asked the author a question or requested changes
feat: Move variational calculus
RFC
Request for comment
#1018
opened Apr 1, 2026 by
jstoobysmith
Member
Loading…
feat: Adds a diffeormorphism for the harmonic oscillator
awaiting-author
A reviewer has asked the author a question or requested changes
#1004
opened Mar 25, 2026 by
jstoobysmith
Member
Loading…
feat(LaplaceRungeLenzVector): prove A reviewer has asked the author a question or requested changes
angularMomentum_commutation_lrl
awaiting-author
#991
opened Mar 14, 2026 by
pitmonticone
Member
Loading…
feat(Pseudo-Riemannian/Lorentzian): major refactor / add Lorentzian metric
#968
opened Mar 3, 2026 by
or4nge19
Collaborator
Loading…
feat(SolidSphere): prove A reviewer has asked the author a question or requested changes
solidSphere_inertiaTensor
awaiting-author
#962
opened Feb 25, 2026 by
pitmonticone
Member
Loading…
Previous Next
ProTip!
Filter pull requests by the default branch with base:master.