Defs

📁 Source: Mathlib/Algebra/LieRinehartAlgebra/Defs.lean

Statistics

Metric	Count
Definitions LieRinehartAlgebra, comp, id, instCoeFunForall, toLieHom, toLinearMap', anchor, «term_→ₗ⁅_⁆_», LieRinehartRing	9
Theorems apply_lie, apply_lie', map_smul_apply, map_smul_apply', toLinearMap'_apply, leibniz_mul_right, leibniz_smul_right, lie_smul_eq_mul, anchor_apply, anchor_derivation, instDerivation, instLieRinehartRingDerivation, toIsScalarTower, toLieModule, leibniz_mul_right', leibniz_smul_right', lie_smul_eq_mul'	17
Total	26

LieRinehartAlgebra

Definitions

Name	Category	Theorems
anchor 📖	CompOp	2 math math: anchor_apply, anchor_derivation
«term_→ₗ⁅_⁆_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anchor_apply 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instFunLike LieHom Derivation.instLieRing Derivation.instLieAlgebra LieHom.instFunLike Hom.toLieHom AlgHom.id CommSemiring.toSemiring Derivation.instModule Algebra.to_smulCommClass Derivation.instLieRingModule anchor Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup	—	Algebra.to_smulCommClass
anchor_derivation 📖	mathematical	—	anchor Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instLieRing Derivation.instModule CommSemiring.toSemiring Algebra.to_smulCommClass Derivation.instLieRingModule Derivation.instLieAlgebra instLieRinehartRingDerivation instDerivation Hom.id	—	Algebra.to_smulCommClass instLieRinehartRingDerivation instDerivation
instDerivation 📖	mathematical	—	LieRinehartAlgebra Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instLieRing Derivation.instModule CommSemiring.toSemiring Algebra.to_smulCommClass Derivation.instLieRingModule instLieRinehartRingDerivation Derivation.instLieAlgebra	—	Algebra.to_smulCommClass instLieRinehartRingDerivation Derivation.instIsScalarTower IsScalarTower.right Derivation.instLieModule
instLieRinehartRingDerivation 📖	mathematical	—	LieRinehartRing Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Derivation.instLieRing Derivation.instModule CommSemiring.toSemiring Algebra.to_smulCommClass Derivation.instLieRingModule	—	Algebra.to_smulCommClass Derivation.leibniz AddLeftCancelSemigroup.toIsLeftCancelAdd Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Derivation.ext Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt
toIsScalarTower 📖	mathematical	—	IsScalarTower Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid LieAlgebra.toModule	—	—
toLieModule 📖	mathematical	—	LieModule LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.toModule LieAlgebra.ofAssociativeAlgebra	—	—

LieRinehartAlgebra.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	—
id 📖	CompOp	1 math math: LieRinehartAlgebra.anchor_derivation
instCoeFunForall 📖	CompOp	—
toLieHom 📖	CompOp	6 math math: map_smul_apply', LieRinehartAlgebra.anchor_apply, map_smul_apply, apply_lie', toLinearMap'_apply, apply_lie
toLinearMap' 📖	CompOp	1 math math: toLinearMap'_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_lie 📖	mathematical	—	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing LieHom LieHom.instFunLike toLieHom	—	apply_lie'
apply_lie' 📖	mathematical	—	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing LieHom LieHom.instFunLike toLieHom	—	—
map_smul_apply 📖	mathematical	—	DFunLike.coe LieHom LieHom.instFunLike toLieHom SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AlgHom AlgHom.funLike	—	map_smul_apply'
map_smul_apply' 📖	mathematical	—	DFunLike.coe LieHom LieHom.instFunLike toLieHom SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AlgHom AlgHom.funLike	—	—
toLinearMap'_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring AlgHom.toRingHom AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LinearMap.instFunLike toLinearMap' LieHom LieHom.instFunLike toLieHom	—	—

LieRinehartAlgebra.LieRinehartRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leibniz_mul_right 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	LieRinehartRing.leibniz_mul_right'
leibniz_smul_right 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LieRing.ofAssociativeRing CommRing.toRing	—	LieRinehartRing.leibniz_smul_right'
lie_smul_eq_mul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing 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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieRinehartRing.lie_smul_eq_mul'

LieRinehartRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leibniz_mul_right' 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	—
leibniz_smul_right' 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LieRing.ofAssociativeRing CommRing.toRing	—	—
lie_smul_eq_mul' 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing 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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—

(root)

Definitions

Name	Category	Theorems
LieRinehartAlgebra 📖	CompData	1 math math: LieRinehartAlgebra.instDerivation
LieRinehartRing 📖	CompData	1 math math: LieRinehartAlgebra.instLieRinehartRingDerivation

---

← Back to Index