Basic

📁 Source: Mathlib/Algebra/Lie/Derivation/Basic.lean

Statistics

Metric	Count
Definitions `LieDerivation`, `SMulBracketCommClass`, `apply`, `coeFnAddMonoidHom`, `exp`, `inner`, `instAdd`, `instAddCommGroup`, `instBracket`, `instCoeToLinearMap`, `instDistribMulAction`, `instFunLike`, `instInhabited`, `instLieAlgebra`, `instLieRing`, `instLieRingModule`, `instModule`, `instNeg`, `instSMul`, `instSub`, `instZero`, `toLinearMap`, `toLinearMapLieHom`	23
Theorems `smul_bracket_comm`, `add_apply`, `apply_lie_eq_add`, `apply_lie_eq_sub`, `coeFnAddMonoidHom_apply`, `coeFn_coe`, `coe_add`, `coe_add_linearMap`, `coe_injective`, `coe_neg`, `coe_neg_linearMap`, `coe_smul`, `coe_smul_linearMap`, `coe_sub`, `coe_sub_linearMap`, `coe_zero`, `coe_zero_linearMap`, `commutator_apply`, `commutator_coe_linear_map`, `congr_fun`, `eqOn_lieSpan`, `exp_apply`, `exp_map_apply`, `ext`, `ext_iff`, `ext_of_lieSpan_eq_top`, `inner_apply_apply`, `instIsScalarTower`, `instLieModule`, `instLinearMapClass`, `instNoetherian`, `instSMulBase`, `instSMulCommClass`, `instSMulInt`, `instSMulNat`, `iterate_apply_lie`, `iterate_apply_lie'`, `leibniz'`, `leibniz_lie`, `lie_apply`, `lie_coe_lieDerivation_apply`, `lie_lieDerivation_apply`, `map_neg`, `map_sub`, `mk_coe`, `neg_apply`, `smul_apply`, `sub_apply`, `toFun_eq_coe`, `toLinearMapLieHom_injective`, `zero_apply`	51
Total	74

LieDerivation

Definitions

Name	Category	Theorems
`SMulBracketCommClass` 📖	CompData	3 math math: `instSMulNat`, `instSMulInt`, `instSMulBase`
`coeFnAddMonoidHom` 📖	CompOp	1 math math: `coeFnAddMonoidHom_apply`
`exp` 📖	CompOp	2 math math: `exp_map_apply`, `exp_apply`
`inner` 📖	CompOp	1 math math: `inner_apply_apply`
`instAdd` 📖	CompOp	4 math math: `coe_add`, `leibniz_lie`, `add_apply`, `coe_add_linearMap`
`instAddCommGroup` 📖	CompOp	11 math math: `instNoetherian`, `ad_apply_lieDerivation`, `inner_apply_apply`, `lie_lieDerivation_apply`, `coeFnAddMonoidHom_apply`, `leibniz_lie`, `lie_coe_lieDerivation_apply`, `IsKilling.rangeAdOrthogonal_carrier`, `lie_ad`, `instLieModule`, `maxTrivSubmodule_eq_bot_of_center_eq_bot`
`instBracket` 📖	CompOp	6 math math: `lie_der_ad_eq_ad_der`, `commutator_apply`, `leibniz_lie`, `lie_apply`, `commutator_coe_linear_map`, `lie_ad`
`instCoeToLinearMap` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instFunLike` 📖	CompOp	33 math math: `IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal`, `coe_smul`, `lie_der_ad_eq_ad_der`, `ad_apply_lieDerivation`, `iterate_apply_lie`, `zero_apply`, `coe_add`, `apply_lie_eq_add`, `inner_apply_apply`, `commutator_apply`, `ext_iff`, `mk_coe`, `map_sub`, `lie_lieDerivation_apply`, `IsKilling.ad_mem_orthogonal_of_mem_orthogonal`, `coe_neg`, `coeFnAddMonoidHom_apply`, `lie_apply`, `neg_apply`, `coe_injective`, `map_neg`, `add_apply`, `congr_fun`, `smul_apply`, `apply_lie_eq_sub`, `coe_zero`, `coe_sub`, `instLinearMapClass`, `coeFn_coe`, `toFun_eq_coe`, `iterate_apply_lie'`, `sub_apply`, `ad_apply_apply`
`instInhabited` 📖	CompOp	—
`instLieAlgebra` 📖	CompOp	16 math math: `lie_der_ad_eq_ad_der`, `ad_apply_lieDerivation`, `IsKilling.instIsKilling_range_ad`, `IsKilling.exists_eq_ad`, `IsKilling.killingForm_restrict_range_ad`, `toLinearMapLieHom_injective`, `ad_isIdealMorphism`, `IsKilling.range_ad_eq_top`, `lie_ad`, `IsKilling.ad_apply_eq_zero_iff`, `injective_ad_of_center_eq_bot`, `coe_ad_apply_eq_ad_apply`, `ad_ker_eq_center`, `mem_ad_idealRange_iff`, `IsKilling.killingForm_restrict_range_ad_nondegenerate`, `ad_apply_apply`
`instLieRing` 📖	CompOp	16 math math: `lie_der_ad_eq_ad_der`, `ad_apply_lieDerivation`, `IsKilling.instIsKilling_range_ad`, `IsKilling.exists_eq_ad`, `IsKilling.killingForm_restrict_range_ad`, `toLinearMapLieHom_injective`, `ad_isIdealMorphism`, `IsKilling.range_ad_eq_top`, `lie_ad`, `IsKilling.ad_apply_eq_zero_iff`, `injective_ad_of_center_eq_bot`, `coe_ad_apply_eq_ad_apply`, `ad_ker_eq_center`, `mem_ad_idealRange_iff`, `IsKilling.killingForm_restrict_range_ad_nondegenerate`, `ad_apply_apply`
`instLieRingModule` 📖	CompOp	8 math math: `ad_apply_lieDerivation`, `lie_lieDerivation_apply`, `leibniz_lie`, `lie_coe_lieDerivation_apply`, `IsKilling.rangeAdOrthogonal_carrier`, `lie_ad`, `instLieModule`, `maxTrivSubmodule_eq_bot_of_center_eq_bot`
`instModule` 📖	CompOp	5 math math: `instNoetherian`, `inner_apply_apply`, `IsKilling.rangeAdOrthogonal_carrier`, `instLieModule`, `maxTrivSubmodule_eq_bot_of_center_eq_bot`
`instNeg` 📖	CompOp	4 math math: `ad_apply_lieDerivation`, `coe_neg_linearMap`, `coe_neg`, `neg_apply`
`instSMul` 📖	CompOp	5 math math: `coe_smul`, `instSMulCommClass`, `instIsScalarTower`, `coe_smul_linearMap`, `smul_apply`
`instSub` 📖	CompOp	3 math math: `coe_sub_linearMap`, `coe_sub`, `sub_apply`
`instZero` 📖	CompOp	4 math math: `zero_apply`, `coe_zero_linearMap`, `IsKilling.ad_apply_eq_zero_iff`, `coe_zero`
`toLinearMap` 📖	CompOp	11 math math: `coe_sub_linearMap`, `coe_neg_linearMap`, `coe_smul_linearMap`, `coe_zero_linearMap`, `lie_coe_lieDerivation_apply`, `commutator_coe_linear_map`, `leibniz'`, `coe_add_linearMap`, `coe_ad_apply_eq_ad_apply`, `coeFn_coe`, `toFun_eq_coe`
`toLinearMapLieHom` 📖	CompOp	1 math math: `toLinearMapLieHom_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`apply_lie_eq_add` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instFunLike` `Bracket.bracket` `LieRingModule.toBracket` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`lieAlgebraSelfModule` `apply_lie_eq_sub` `sub_eq_add_neg` `lie_skew`
`apply_lie_eq_sub` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`leibniz'`
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `LieDerivation` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLike`	—	—
`coeFn_coe` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instFunLike` `toLinearMap` `LieDerivation` `instFunLike`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instAdd` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`coe_add_linearMap` 📖	mathematical	—	`toLinearMap` `LieDerivation` `instAdd` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instAdd`	—	—
`coe_injective` 📖	mathematical	—	`LieDerivation` `DFunLike.coe` `instFunLike`	—	`DFunLike.coe_injective`
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`coe_neg_linearMap` 📖	mathematical	—	`toLinearMap` `LieDerivation` `instNeg` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instNeg`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`coe_smul_linearMap` 📖	mathematical	—	`toLinearMap` `LieDerivation` `instSMul` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_sub_linearMap` 📖	mathematical	—	`toLinearMap` `LieDerivation` `instSub` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instSub`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instZero` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`coe_zero_linearMap` 📖	mathematical	—	`toLinearMap` `LieDerivation` `instZero` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero`	—	—
`commutator_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instFunLike` `Bracket.bracket` `instBracket` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`lieAlgebraSelfModule`
`commutator_coe_linear_map` 📖	mathematical	—	`toLinearMap` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `Bracket.bracket` `LieDerivation` `instBracket` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRingModule.toBracket` `LieRing.ofAssociativeRing` `Module.End.instRing` `LinearMap.addCommGroup` `LinearMap.instLieRingModule` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.End.instLieRingModule` `Module.End.instLieModule`	—	`lieAlgebraSelfModule`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike`	—	`DFunLike.congr_fun`
`eqOn_lieSpan` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `LieDerivation` `instFunLike`	`SetLike.coe` `LieSubalgebra` `LieSubalgebra.instSetLike` `LieSubalgebra.lieSpan`	—	`LieSubalgebra.lieSpan_induction` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `instLinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `apply_lie_eq_sub`
`exp_apply` 📖	mathematical	`IsNilpotent` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero` `Monoid.toNatPow` `Module.End.instMonoid` `toLinearMap` `lieRingSelfModule` `lieAlgebraSelfModule`	`LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LieEquiv.toLinearEquiv` `exp` `IsNilpotent.exp` `Module.End.instRing` `LinearMap.module` `Rat.semiring` `Rat.commRing` `SMulCommClass.rat'` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction`	—	`lieAlgebraSelfModule` `RingHomInvPair.ids`
`exp_map_apply` 📖	mathematical	`IsNilpotent` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero` `Monoid.toNatPow` `Module.End.instMonoid` `toLinearMap` `lieRingSelfModule` `lieAlgebraSelfModule`	`DFunLike.coe` `LieEquiv` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `exp` `LinearMap.instFunLike` `IsNilpotent.exp` `Module.End.instRing` `LinearMap.module` `Rat.semiring` `Rat.commRing` `SMulCommClass.rat'` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction`	—	`lieAlgebraSelfModule` `DFunLike.congr_fun` `RingHomInvPair.ids` `SMulCommClass.rat'` `exp_apply`
`ext` 📖	—	`DFunLike.coe` `LieDerivation` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike`	—	`ext`
`ext_of_lieSpan_eq_top` 📖	—	`LieSubalgebra.lieSpan` `Top.top` `LieSubalgebra` `LieSubalgebra.instTop` `Set.EqOn` `DFunLike.coe` `LieDerivation` `instFunLike`	—	—	`ext` `eqOn_lieSpan`
`inner_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instSMulBase` `LinearMap.instFunLike` `inner` `Bracket.bracket` `LieRingModule.toBracket`	—	`smulCommClass_self` `instSMulBase`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `LieDerivation` `instSMul`	—	`ext` `smul_assoc`
`instLieModule` 📖	mathematical	—	`LieModule` `LieDerivation` `instAddCommGroup` `instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instSMulBase` `instLieRingModule`	—	`smulCommClass_self` `instSMulBase` `ext` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `instLinearMapClass` `lie_smul`
`instLinearMapClass` 📖	mathematical	—	`LinearMapClass` `LieDerivation` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `instFunLike`	—	`AddHom.map_add'` `LinearMap.map_smul`
`instNoetherian` 📖	mathematical	—	`IsNoetherian` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instSMulBase`	—	`isNoetherian_of_linearEquiv` `smulCommClass_self` `IsScalarTower.left` `lieAlgebraSelfModule` `RingHomSurjective.invPair` `RingHomInvPair.ids` `instSMulBase` `toLinearMapLieHom_injective` `isNoetherian_submodule'` `isNoetherian_linearMap` `Module.IsNoetherian.finite`
`instSMulBase` 📖	mathematical	—	`SMulBracketCommClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`lie_smul`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `LieDerivation` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`instSMulInt` 📖	mathematical	—	`SMulBracketCommClass` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`lie_zsmul`
`instSMulNat` 📖	mathematical	—	`SMulBracketCommClass` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`lie_nsmul`
`iterate_apply_lie` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instFunLike` `Bracket.bracket` `LieRingModule.toBracket` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Nat.choose`	—	`lieAlgebraSelfModule` `Finset.sum_congr` `Finset.antidiagonal_zero` `Nat.instCanonicallyOrderedAdd` `Finset.sum_singleton` `Nat.choose_self` `one_smul` `Finset.sum_antidiagonal_choose_succ_nsmul` `Function.iterate_succ_apply'` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `instLinearMapClass` `map_nsmul` `apply_lie_eq_add` `smul_add` `Finset.sum_add_distrib` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.choose_symm_of_eq_add` `Finset.HasAntidiagonal.mem_antidiagonal`
`iterate_apply_lie'` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instFunLike` `Bracket.bracket` `LieRingModule.toBracket` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.range` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Nat.choose`	—	`lieAlgebraSelfModule` `iterate_apply_lie` `Finset.Nat.sum_antidiagonal_eq_sum_range_succ`
`leibniz'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instFunLike` `toLinearMap` `Bracket.bracket` `LieRingModule.toBracket` `lieRingSelfModule` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`leibniz_lie` 📖	mathematical	—	`Bracket.bracket` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieRingModule.toBracket` `instAddCommGroup` `instLieRingModule` `instBracket` `instAdd`	—	`lieAlgebraSelfModule` `ext` `sub_eq_neg_add` `lie_add` `lie_neg` `apply_lie_eq_sub` `lie_skew` `neg_neg` `neg_add_rev` `neg_add_cancel_right` `neg_add_cancel_left`
`lie_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instFunLike` `Bracket.bracket` `instBracket` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`lieAlgebraSelfModule`
`lie_coe_lieDerivation_apply` 📖	mathematical	—	`Bracket.bracket` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieRingModule.toBracket` `LinearMap.addCommGroup` `LinearMap.instLieRingModule` `lieRingSelfModule` `lieAlgebraSelfModule` `toLinearMap` `LieDerivation` `instAddCommGroup` `instLieRingModule`	—	`LinearMap.ext` `lieAlgebraSelfModule` `apply_lie_eq_sub` `sub_sub_cancel`
`lie_lieDerivation_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `Bracket.bracket` `LieRingModule.toBracket` `instAddCommGroup` `instLieRingModule`	—	—
`map_neg` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `instLinearMapClass`
`map_sub` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LieRing.toAddCommGroup`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `instLinearMapClass`
`mk_coe` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instFunLike` `Bracket.bracket` `LieRingModule.toBracket` `lieRingSelfModule` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`LieDerivation` `instFunLike`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`toFun_eq_coe` 📖	mathematical	—	`AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LinearMap.toAddHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LieAlgebra.toModule` `toLinearMap` `DFunLike.coe` `LieDerivation` `instFunLike`	—	—
`toLinearMapLieHom_injective` 📖	mathematical	—	`LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LieHom` `instLieRing` `instLieAlgebra` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `toLinearMapLieHom`	—	`lieAlgebraSelfModule` `smulCommClass_self` `IsScalarTower.left` `ext`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `instFunLike` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—

LieDerivation.SMulBracketCommClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_bracket_comm` 📖	mathematical	—	`Bracket.bracket` `LieRingModule.toBracket`	—	—

LieDerivation.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`LieDerivation` 📖	CompData	58 math math: `LieDerivation.coe_smul`, `LieDerivation.lie_der_ad_eq_ad_der`, `LieDerivation.instNoetherian`, `LieDerivation.ad_apply_lieDerivation`, `LieDerivation.iterate_apply_lie`, `LieDerivation.IsKilling.instIsKilling_range_ad`, `LieDerivation.zero_apply`, `LieDerivation.coe_sub_linearMap`, `LieDerivation.instSMulCommClass`, `LieDerivation.IsKilling.exists_eq_ad`, `LieDerivation.coe_add`, `LieDerivation.apply_lie_eq_add`, `LieDerivation.inner_apply_apply`, `LieDerivation.commutator_apply`, `LieDerivation.instIsScalarTower`, `LieDerivation.coe_neg_linearMap`, `LieDerivation.coe_smul_linearMap`, `LieDerivation.ext_iff`, `LieDerivation.IsKilling.killingForm_restrict_range_ad`, `LieDerivation.mk_coe`, `LieDerivation.map_sub`, `LieDerivation.lie_lieDerivation_apply`, `LieDerivation.coe_neg`, `LieDerivation.coe_zero_linearMap`, `LieDerivation.coeFnAddMonoidHom_apply`, `LieDerivation.leibniz_lie`, `LieDerivation.lie_apply`, `LieDerivation.neg_apply`, `LieDerivation.toLinearMapLieHom_injective`, `LieDerivation.ad_isIdealMorphism`, `LieDerivation.lie_coe_lieDerivation_apply`, `LieDerivation.IsKilling.rangeAdOrthogonal_carrier`, `LieDerivation.commutator_coe_linear_map`, `LieDerivation.coe_injective`, `LieDerivation.IsKilling.range_ad_eq_top`, `LieDerivation.lie_ad`, `LieDerivation.map_neg`, `LieDerivation.add_apply`, `LieDerivation.congr_fun`, `LieDerivation.IsKilling.ad_apply_eq_zero_iff`, `LieDerivation.smul_apply`, `LieDerivation.apply_lie_eq_sub`, `LieDerivation.injective_ad_of_center_eq_bot`, `LieDerivation.instLieModule`, `LieDerivation.coe_add_linearMap`, `LieDerivation.coe_zero`, `LieDerivation.coe_sub`, `LieDerivation.coe_ad_apply_eq_ad_apply`, `LieDerivation.ad_ker_eq_center`, `LieDerivation.mem_ad_idealRange_iff`, `LieDerivation.instLinearMapClass`, `LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate`, `LieDerivation.coeFn_coe`, `LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot`, `LieDerivation.toFun_eq_coe`, `LieDerivation.iterate_apply_lie'`, `LieDerivation.sub_apply`, `LieDerivation.ad_apply_apply`

---

← Back to Index