Documentation Verification Report

BaseChange

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

Statistics

Metric	Count
Definitions `ofDerivation`, `ofLieDerivation`	2
Theorems `ofDerivation_apply`, `ofLieDerivation_apply`	2
Total	4

Lie.Derivation

Definitions

Name	Category	Theorems
`ofDerivation` 📖	CompOp	1 math math: `ofDerivation_apply`
`ofLieDerivation` 📖	CompOp	1 math math: `ofLieDerivation_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofDerivation_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `LieAlgebra.ExtendScalars.instLieRing` `LieAlgebra.ExtendScalars.instBaseLieAlgebra` `TensorProduct.addCommGroup` `TensorProduct.instModule` `LieAlgebra.ExtendScalars.instLieRingModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieDerivation.instFunLike` `LieHom` `Derivation` `Algebra.id` `Derivation.instLieRing` `Derivation.instLieAlgebra` `LieDerivation.instLieRing` `LieDerivation.instLieAlgebra` `LieHom.instFunLike` `ofDerivation` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `LinearMap.instFunLike` `LinearMap.rTensor` `Derivation.toLinearMap`	—	`lieAlgebraSelfModule`
`ofLieDerivation_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `LieAlgebra.ExtendScalars.instLieRing` `LieAlgebra.ExtendScalars.instBaseLieAlgebra` `TensorProduct.addCommGroup` `TensorProduct.instModule` `LieAlgebra.ExtendScalars.instLieRingModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieDerivation.instFunLike` `LieHom` `LieDerivation.instLieRing` `LieDerivation.instLieAlgebra` `LieHom.instFunLike` `ofLieDerivation` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `LinearMap.instFunLike` `LinearMap.lTensor` `LieDerivation.toLinearMap`	—	`lieAlgebraSelfModule`

---

← Back to Index