feat(PhyslibAlpha): the mass cocycle of the Galilean group (Souriau) - #1687

Open

KevorkianPhilippe wants to merge 9 commits into

leanprover-community:masterfrom

KevorkianPhilippe:galilee-2

Commits on Sep 24, 2026

feat(PhyslibAlpha/ClassicalMechanics): the mass as a cohomology class of the Galilean Lie algebra

Philippe Kevorkian
and
claude
committed
c7d4f8b
feat(PhyslibAlpha/ClassicalMechanics): the mass cocycle of the Galilean group

Philippe Kevorkian
and
claude
committed
1a8ee8c
feat(PhyslibAlpha/ClassicalMechanics): state the mass cocycle results on Souriau's group SO(3)

Philippe Kevorkian
and
claude
committed
67c3d7f
docs(PhyslibAlpha/ClassicalMechanics): GalileanMass docstrings after a read-back against the book

Philippe Kevorkian
and
claude
committed
d45d65c
Merge branch 'galilee-1' into galilee-2
Philippe Kevorkian
committed
c6b5074

Commits on Sep 25, 2026

Merge remote-tracking branch 'origin/master' into galilee-1

Philippe Kevorkian
and
claude
committed
fb5250d
refactor(PhyslibAlpha/ClassicalMechanics): move the moment map files into MomentMap/

Philippe Kevorkian
and
claude
committed
ae21c03
Merge branch 'galilee-1' into galilee-2

Philippe Kevorkian
and
claude
committed
f691590
refactor(PhyslibAlpha/ClassicalMechanics): move GalileanMassCocycle.lean into MomentMap/

Philippe Kevorkian
and
claude
committed
1e6c267