Skip to content

Pull requests: leanprover-community/physlib

Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort

Pull requests list

feat(QM): Add SpaceDQuantumSystem t-quantum-mechanics Quantum mechanics
#1114 opened May 21, 2026 by gloges Contributor Loading…
feat: Other implementation
#1111 opened May 20, 2026 by jstoobysmith Member Draft
feat(QuantumMechanics): sudden frequency change for the QHO
#1109 opened May 19, 2026 by casualPhysics Collaborator Loading…
6 tasks done
feat: TensorSpecies.ofFunction
#1100 opened May 15, 2026 by jstoobysmith Member 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: QuantumInfo sorryful results
#1092 opened May 12, 2026 by jstoobysmith Member 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
#1039 opened Apr 15, 2026 by juanjfndz Contributor Draft
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 angularMomentum_commutation_lrl awaiting-author A reviewer has asked the author a question or requested changes
#991 opened Mar 14, 2026 by pitmonticone Member Loading…
feat(temperature): PositiveTemperature refactor t-thermodynamics Thermodynamics
#976 opened Mar 5, 2026 by ichxorya Contributor Draft
feat(SolidSphere): prove solidSphere_inertiaTensor awaiting-author A reviewer has asked the author a question or requested changes
#962 opened Feb 25, 2026 by pitmonticone Member Loading…
ProTip! Filter pull requests by the default branch with base:master.