Commit 2026-03-18 16:52 2f6dd10c

View on Github →

feat: added simp lemmas to LieRinehartAlgebra (#36650) This pull request adds simp lemmas for the defining properties of Lie-Rinehart-Algebras. Additionally the definition of anchor is moved out of the Hom namespace. (Even though the anchor itself is a Hom, it is an object associated to an LR-algebra, not a Hom of algebras).

Estimated changes

Modified Mathlib/Algebra/LieRinehartAlgebra/Defs.lean

deleted def LieRinehartAlgebra.Hom.anchor

deleted theorem LieRinehartAlgebra.Hom.anchor_derivation

added theorem LieRinehartAlgebra.LieRinehartRing.leibniz_mul_right

added theorem LieRinehartAlgebra.LieRinehartRing.leibniz_smul_right

added theorem LieRinehartAlgebra.LieRinehartRing.lie_smul_eq_mul

added def LieRinehartAlgebra.anchor

added theorem LieRinehartAlgebra.anchor_apply

added theorem LieRinehartAlgebra.anchor_derivation