Documentation Verification Report

Defs

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

Statistics

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

LieRinehartAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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
`anchor` 📖	CompOp	1 math math: `anchor_derivation`
`comp` 📖	CompOp	—
`id` 📖	CompOp	1 math math: `anchor_derivation`
`instCoeFunForall` 📖	CompOp	—
`toLieHom` 📖	CompOp	5 math math: `map_smul_apply'`, `map_smul_apply`, `apply_lie'`, `toLinearMap'_apply`, `apply_lie`
`toLinearMap'` 📖	CompOp	1 math math: `toLinearMap'_apply`
`«term_→ₗ⁅_⁆_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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` `LieRinehartAlgebra.instLieRinehartRingDerivation` `LieRinehartAlgebra.instDerivation` `id`	—	`Algebra.to_smulCommClass` `LieRinehartAlgebra.instLieRinehartRingDerivation` `LieRinehartAlgebra.instDerivation`
`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`	—	—

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