Commit 2026-07-28 15:02 5b20aff7

View on Github →

feat(Algebra/Lie): use IsApply for Weight (#42129)

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

deleted theorem LieModule.Weight.coe_zero

deleted theorem LieModule.Weight.zero_apply

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean