Documentation Verification Report

UniversalEnveloping

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

Statistics

Metric	Count
Definitions `UniversalEnvelopingAlgebra`, `mkAlgHom`, `ι`, `instAlgebraUniversalEnvelopingAlgebra`, `instInhabitedUniversalEnvelopingAlgebra`, `instRingUniversalEnvelopingAlgebra`	6
Theorems `hom_ext`, `hom_ext_iff`, `lift_symm_apply`, `lift_unique`, `lift_ι_apply`, `lift_ι_apply'`, `ι_apply`, `ι_comp_lift`	8
Total	14

UniversalEnvelopingAlgebra

Definitions

Name	Category	Theorems
`mkAlgHom` 📖	CompOp	2 math math: `ι_apply`, `lift_ι_apply'`
`ι` 📖	CompOp	7 math math: `lift_unique`, `ι_comp_lift`, `lift_ι_apply`, `lift_symm_apply`, `ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`LieHom.comp` `UniversalEnvelopingAlgebra` `LieRing.ofAssociativeRing` `instRingUniversalEnvelopingAlgebra` `LieAlgebra.ofAssociativeAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `AlgHom.toLieHom` `ι`	—	—	`Equiv.injective`
`hom_ext_iff` 📖	mathematical	—	`LieHom.comp` `UniversalEnvelopingAlgebra` `LieRing.ofAssociativeRing` `instRingUniversalEnvelopingAlgebra` `LieAlgebra.ofAssociativeAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `AlgHom.toLieHom` `ι`	—	`hom_ext`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `UniversalEnvelopingAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `LieHom` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `LieHom.comp` `AlgHom.toLieHom` `ι`	—	—
`lift_unique` 📖	mathematical	—	`UniversalEnvelopingAlgebra` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `AlgHom.funLike` `LieHom` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `LieHom.instFunLike` `ι` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`LieHom.ext` `Equiv.symm_apply_eq`
`lift_ι_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `UniversalEnvelopingAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `AlgHom.funLike` `Equiv` `LieHom` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `LieHom.instFunLike` `ι`	—	`ι_comp_lift`
`lift_ι_apply'` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `UniversalEnvelopingAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `AlgHom.funLike` `Equiv` `LieHom` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `instSemiringTensorAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `mkAlgHom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `TensorAlgebra.ι` `LieHom.instFunLike`	—	`lift_ι_apply`
`ι_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `UniversalEnvelopingAlgebra` `LieRing.ofAssociativeRing` `instRingUniversalEnvelopingAlgebra` `LieAlgebra.ofAssociativeAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `LieHom.instFunLike` `ι` `AlgHom` `TensorAlgebra` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `instSemiringTensorAlgebra` `Ring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `mkAlgHom` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `TensorAlgebra.ι`	—	—
`ι_comp_lift` 📖	mathematical	—	`UniversalEnvelopingAlgebra` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingUniversalEnvelopingAlgebra` `instAlgebraUniversalEnvelopingAlgebra` `AlgHom.funLike` `Equiv` `LieHom` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `LieHom.instFunLike` `ι`	—	`LieHom.ext_iff` `Equiv.symm_apply_apply`

(root)

Definitions

Name	Category	Theorems
`UniversalEnvelopingAlgebra` 📖	CompOp	9 math math: `UniversalEnvelopingAlgebra.lift_unique`, `UniversalEnvelopingAlgebra.ι_comp_lift`, `UniversalEnvelopingAlgebra.lift_ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `UniversalEnvelopingAlgebra.lift_symm_apply`, `UniversalEnvelopingAlgebra.ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `UniversalEnvelopingAlgebra.hom_ext_iff`, `UniversalEnvelopingAlgebra.lift_ι_apply'`
`instAlgebraUniversalEnvelopingAlgebra` 📖	CompOp	9 math math: `UniversalEnvelopingAlgebra.lift_unique`, `UniversalEnvelopingAlgebra.ι_comp_lift`, `UniversalEnvelopingAlgebra.lift_ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `UniversalEnvelopingAlgebra.lift_symm_apply`, `UniversalEnvelopingAlgebra.ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `UniversalEnvelopingAlgebra.hom_ext_iff`, `UniversalEnvelopingAlgebra.lift_ι_apply'`
`instInhabitedUniversalEnvelopingAlgebra` 📖	CompOp	—
`instRingUniversalEnvelopingAlgebra` 📖	CompOp	9 math math: `UniversalEnvelopingAlgebra.lift_unique`, `UniversalEnvelopingAlgebra.ι_comp_lift`, `UniversalEnvelopingAlgebra.lift_ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply`, `UniversalEnvelopingAlgebra.lift_symm_apply`, `UniversalEnvelopingAlgebra.ι_apply`, `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply`, `UniversalEnvelopingAlgebra.hom_ext_iff`, `UniversalEnvelopingAlgebra.lift_ι_apply'`

---

← Back to Index