Documentation Verification Report

Free

📁 Source: Mathlib/Algebra/Lie/Free.lean

Statistics

Metric	Count
Definitions `FreeLieAlgebra`, `instAdd`, `instAddCommGroup`, `instAddCommSemigroup`, `instAddGroup`, `instLieAlgebra`, `instLieRing`, `instModuleOfIsScalarTower`, `instNeg`, `instSMulOfIsScalarTower`, `instSub`, `instZero`, `liftAux`, `mk`, `of`, `universalEnvelopingEquivFreeAlgebra`, `instInhabitedFreeLieAlgebra`	17
Theorems `addLeft`, `neg`, `smulOfTower`, `subLeft`, `subRight`, `hom_ext`, `hom_ext_iff`, `instIsCentralScalar`, `liftAux_map_add`, `liftAux_map_mul`, `liftAux_map_smul`, `liftAux_spec`, `lift_comp_of`, `lift_of_apply`, `lift_symm_apply`, `lift_unique`, `of_comp_lift`, `universalEnvelopingEquivFreeAlgebra_apply`, `universalEnvelopingEquivFreeAlgebra_symm_apply`	19
Total	36

FreeLieAlgebra

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	—
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instLieAlgebra` 📖	CompOp	8 math math: `of_comp_lift`, `lift_comp_of`, `lift_unique`, `universalEnvelopingEquivFreeAlgebra_apply`, `hom_ext_iff`, `universalEnvelopingEquivFreeAlgebra_symm_apply`, `lift_symm_apply`, `lift_of_apply`
`instLieRing` 📖	CompOp	8 math math: `of_comp_lift`, `lift_comp_of`, `lift_unique`, `universalEnvelopingEquivFreeAlgebra_apply`, `hom_ext_iff`, `universalEnvelopingEquivFreeAlgebra_symm_apply`, `lift_symm_apply`, `lift_of_apply`
`instModuleOfIsScalarTower` 📖	CompOp	—
`instNeg` 📖	CompOp	—
`instSMulOfIsScalarTower` 📖	CompOp	1 math math: `instIsCentralScalar`
`instSub` 📖	CompOp	—
`instZero` 📖	CompOp	—
`liftAux` 📖	CompOp	4 math math: `liftAux_map_smul`, `liftAux_map_add`, `liftAux_map_mul`, `liftAux_spec`
`mk` 📖	CompOp	—
`of` 📖	CompOp	7 math math: `of_comp_lift`, `lift_comp_of`, `lift_unique`, `hom_ext_iff`, `universalEnvelopingEquivFreeAlgebra_symm_apply`, `lift_symm_apply`, `lift_of_apply`
`universalEnvelopingEquivFreeAlgebra` 📖	CompOp	2 math math: `universalEnvelopingEquivFreeAlgebra_apply`, `universalEnvelopingEquivFreeAlgebra_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`DFunLike.coe` `LieHom` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `of`	—	—	`Equiv.injective`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `LieHom` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `of`	—	`hom_ext`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `FreeLieAlgebra` `instSMulOfIsScalarTower` `MulOpposite` `MulOpposite.instMonoid` `IsScalarTower.op_left` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`IsScalarTower.op_left` `IsCentralScalar.op_smul_eq_smul` `MonoidAlgebra.isCentralScalar`
`liftAux_map_add` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `FreeNonUnitalNonAssocAlgebra` `CommutatorRing` `MonoidAlgebra.nonUnitalNonAssocSemiring` `FreeMagma` `FreeMagma.instMul` `MonoidAlgebra.distribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instNonUnitalNonAssocRingCommutatorRing` `LieAlgebra.toModule` `LieAlgebra.instLieRingCommutatorRing` `LieAlgebra.instCommutatorRing` `NonUnitalAlgHom.instFunLike_1` `liftAux` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`
`liftAux_map_mul` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `FreeNonUnitalNonAssocAlgebra` `CommutatorRing` `MonoidAlgebra.nonUnitalNonAssocSemiring` `FreeMagma` `FreeMagma.instMul` `MonoidAlgebra.distribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instNonUnitalNonAssocRingCommutatorRing` `LieAlgebra.toModule` `LieAlgebra.instLieRingCommutatorRing` `LieAlgebra.instCommutatorRing` `NonUnitalAlgHom.instFunLike_1` `liftAux` `MonoidAlgebra.instMul` `Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	`map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`
`liftAux_map_smul` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `FreeNonUnitalNonAssocAlgebra` `CommutatorRing` `MonoidAlgebra.nonUnitalNonAssocSemiring` `FreeMagma` `FreeMagma.instMul` `MonoidAlgebra.distribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instNonUnitalNonAssocRingCommutatorRing` `LieAlgebra.toModule` `LieAlgebra.instLieRingCommutatorRing` `LieAlgebra.instCommutatorRing` `NonUnitalAlgHom.instFunLike_1` `liftAux` `SMulZeroClass.toSMul` `AddZero.toZero` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MonoidAlgebra.addCommMonoid` `MonoidAlgebra.smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LieRing.toAddCommGroup` `DistribMulAction.toDistribSMul`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`
`liftAux_spec` 📖	mathematical	`Rel`	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `FreeNonUnitalNonAssocAlgebra` `CommutatorRing` `MonoidAlgebra.nonUnitalNonAssocSemiring` `FreeMagma` `FreeMagma.instMul` `MonoidAlgebra.distribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instNonUnitalNonAssocRingCommutatorRing` `LieAlgebra.toModule` `LieAlgebra.instLieRingCommutatorRing` `LieAlgebra.instCommutatorRing` `NonUnitalAlgHom.instFunLike_1` `liftAux`	—	`liftAux_map_mul` `lie_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `liftAux_map_add` `lie_lie` `sub_add_cancel` `liftAux_map_smul`
`lift_comp_of` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LieHom` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `LieHom.instFunLike` `of`	—	`lift_symm_apply` `Equiv.apply_symm_apply`
`lift_of_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	`of_comp_lift`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LieHom` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `LieHom.instFunLike` `of`	—	—
`lift_unique` 📖	mathematical	—	`FreeLieAlgebra` `DFunLike.coe` `LieHom` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `of` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`Equiv.symm_apply_eq`
`of_comp_lift` 📖	mathematical	—	`FreeLieAlgebra` `DFunLike.coe` `LieHom` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	`Equiv.left_inv`
`universalEnvelopingEquivFreeAlgebra_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `UniversalEnvelopingAlgebra` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `FreeAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `FreeAlgebra.instSemiring` `instAlgebraUniversalEnvelopingAlgebra` `FreeAlgebra.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `universalEnvelopingEquivFreeAlgebra` `AlgHom` `AlgHom.funLike` `Equiv` `LieHom` `LieRing.ofAssociativeRing` `FreeAlgebra.instRing` `LieAlgebra.ofAssociativeAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniversalEnvelopingAlgebra.lift` `lift` `FreeAlgebra.ι`	—	—
`universalEnvelopingEquivFreeAlgebra_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `FreeAlgebra` `CommRing.toCommSemiring` `UniversalEnvelopingAlgebra` `FreeLieAlgebra` `instLieRing` `instLieAlgebra` `FreeAlgebra.instSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `FreeAlgebra.instAlgebra` `Algebra.id` `instAlgebraUniversalEnvelopingAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `universalEnvelopingEquivFreeAlgebra` `AlgHom` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAlgebra.lift` `LieHom` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `LieHom.instFunLike` `UniversalEnvelopingAlgebra.ι` `of`	—	—

FreeLieAlgebra.Rel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft` 📖	mathematical	`FreeLieAlgebra.Rel`	`FreeNonUnitalNonAssocAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `MonoidAlgebra.nonUnitalNonAssocSemiring` `FreeMagma` `FreeMagma.instMul`	—	`add_comm`
`neg` 📖	mathematical	`FreeLieAlgebra.Rel`	`FreeNonUnitalNonAssocAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MonoidAlgebra.addCommGroup` `FreeMagma` `CommRing.toRing`	—	`neg_one_smul`
`smulOfTower` 📖	mathematical	`FreeLieAlgebra.Rel`	`FreeNonUnitalNonAssocAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `MonoidAlgebra` `FreeMagma` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MonoidAlgebra.addCommMonoid` `MonoidAlgebra.smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DistribMulAction.toDistribSMul`	—	`smul_one_smul` `MonoidAlgebra.isScalarTower`
`subLeft` 📖	mathematical	`FreeLieAlgebra.Rel`	`FreeNonUnitalNonAssocAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidAlgebra.addCommGroup` `FreeMagma` `CommRing.toRing`	—	`sub_eq_add_neg` `addLeft` `neg`
`subRight` 📖	mathematical	`FreeLieAlgebra.Rel`	`FreeNonUnitalNonAssocAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidAlgebra.addCommGroup` `FreeMagma` `CommRing.toRing`	—	`sub_eq_add_neg`

(root)

Definitions

Name	Category	Theorems
`FreeLieAlgebra` 📖	CompOp	9 math math: `FreeLieAlgebra.of_comp_lift`, `FreeLieAlgebra.lift_comp_of`, `FreeLieAlgebra.lift_unique`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `FreeLieAlgebra.hom_ext_iff`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `FreeLieAlgebra.lift_symm_apply`, `FreeLieAlgebra.instIsCentralScalar`, `FreeLieAlgebra.lift_of_apply`
`instInhabitedFreeLieAlgebra` 📖	CompOp	—

---

← Back to Index