Commit 2024-04-26 06:26 059a0b64

View on Github →

feat: define Lie module structure on derivations (#12315) Also add some basic consequences

Estimated changes

Modified Mathlib/Algebra/Lie/Derivation/AdjointAction.lean

added theorem LieDerivation.ad_apply_lieDerivation

added theorem LieDerivation.lie_ad

added theorem LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot

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

added theorem LieDerivation.lie_apply

added theorem LieDerivation.lie_coe_lieDerivation_apply

added theorem LieDerivation.lie_lieDerivation_apply

Modified Mathlib/Algebra/Lie/Derivation/Killing.lean