Commit 2023-07-08 04:19 70f24eee

View on Github →

feat: port Geometry.Manifold.Algebra.LeftInvariantDerivation (#5665)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean

added def LeftInvariantDerivation.coeFnAddMonoidHom

added theorem LeftInvariantDerivation.coe_add

added theorem LeftInvariantDerivation.coe_derivation

added theorem LeftInvariantDerivation.coe_injective

added theorem LeftInvariantDerivation.coe_neg

added theorem LeftInvariantDerivation.coe_smul

added theorem LeftInvariantDerivation.coe_sub

added theorem LeftInvariantDerivation.coe_zero

added theorem LeftInvariantDerivation.commutator_apply

added theorem LeftInvariantDerivation.commutator_coe_derivation

added theorem LeftInvariantDerivation.comp_L

added def LeftInvariantDerivation.evalAt

added theorem LeftInvariantDerivation.evalAt_apply

added theorem LeftInvariantDerivation.evalAt_coe

added theorem LeftInvariantDerivation.evalAt_mul

added theorem LeftInvariantDerivation.ext

added theorem LeftInvariantDerivation.left_invariant'

added theorem LeftInvariantDerivation.left_invariant

added theorem LeftInvariantDerivation.leibniz

added theorem LeftInvariantDerivation.lift_add

added theorem LeftInvariantDerivation.lift_smul

added theorem LeftInvariantDerivation.lift_zero

added theorem LeftInvariantDerivation.toDerivation_injective

added theorem LeftInvariantDerivation.toFun_eq_coe

added structure LeftInvariantDerivation

Modified Mathlib/RingTheory/Derivation/Basic.lean