Documentation Verification Report

Quotient

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

Statistics

Metric	Count
Definitions `Quotient`, `quotKerEquivRange`, `actionAsEndoMap`, `actionAsEndoMapBracket`, `addCommGroup`, `inhabited`, `lieQuotientHasBracket`, `lieQuotientLieAlgebra`, `lieQuotientLieRing`, `lieQuotientLieRingModule`, `lieSubmoduleInvariant`, `mk`, `mk'`, `module'`, `instHasQuotient`	15
Theorems `quotKerEquivRange_invFun`, `quotKerEquivRange_toFun`, `isCentralScalar`, `isNoetherian`, `is_quotient_mk`, `lieModuleHom_ext`, `lieModuleHom_ext_iff`, `lieQuotientLieModule`, `map_mk'_eq_bot_le`, `mk'_apply`, `mk'_ker`, `mk_bracket`, `mk_eq_zero`, `mk_eq_zero'`, `range_mk'`, `surjective_mk'`, `toEnd_comp_mk'`	17
Total	32

Algebra.Presentation

Definitions

Name	Category	Theorems
`Quotient` 📖	CompOp	3 math math: `quotientEquiv_symm`, `quotientEquiv_mk`, `instFinitePresentationQuotientOfFinite`

LieHom

Definitions

Name	Category	Theorems
`quotKerEquivRange` 📖	CompOp	2 math math: `quotKerEquivRange_toFun`, `quotKerEquivRange_invFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotKerEquivRange_invFun` 📖	mathematical	—	`LieEquiv.invFun` `HasQuotient.Quotient` `LieIdeal` `LieSubmodule.instHasQuotient` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `ker` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `range` `LieSubmodule.Quotient.lieQuotientLieRing` `LieSubmodule.Quotient.lieQuotientLieAlgebra` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `quotKerEquivRange` `LinearEquiv.invFun` `Ring.toSemiring` `CommRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.ker` `toLinearMap` `Submodule.setLike` `LinearMap.range` `Submodule.Quotient.addCommGroup` `Submodule.addCommMonoid` `Submodule.Quotient.module` `Submodule.module` `LinearMap.quotKerEquivRange`	—	—
`quotKerEquivRange_toFun` 📖	mathematical	—	`DFunLike.coe` `LieEquiv` `HasQuotient.Quotient` `LieIdeal` `LieSubmodule.instHasQuotient` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `ker` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `range` `LieSubmodule.Quotient.lieQuotientLieRing` `LieSubmodule.Quotient.lieQuotientLieAlgebra` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `quotKerEquivRange` `LinearEquiv` `Ring.toSemiring` `CommRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `LinearMap.ker` `toLinearMap` `Submodule.setLike` `LinearMap.range` `Submodule.Quotient.addCommGroup` `Submodule.addCommMonoid` `Submodule.Quotient.module` `Submodule.module` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.quotKerEquivRange`	—	—

LieSubmodule

Definitions

Name	Category	Theorems
`instHasQuotient` 📖	CompOp	18 math math: `Quotient.mk_eq_zero`, `Quotient.mk'_ker`, `LieHom.quotKerEquivRange_toFun`, `Quotient.toEnd_comp_mk'`, `Quotient.range_mk'`, `coe_lowerCentralSeries_ideal_quot_eq`, `LieModule.isNilpotent_quotient_iff`, `Quotient.map_mk'_eq_bot_le`, `Quotient.isCentralScalar`, `LieHom.quotKerEquivRange_invFun`, `Quotient.surjective_mk'`, `Quotient.lieModuleHom_ext_iff`, `Quotient.mk_eq_zero'`, `LieSubalgebra.normalizer_eq_self_iff`, `Quotient.mk_bracket`, `Quotient.lieQuotientLieModule`, `Quotient.isNoetherian`, `Quotient.mk'_apply`

LieSubmodule.Quotient

Definitions

Name	Category	Theorems
`actionAsEndoMap` 📖	CompOp	—
`actionAsEndoMapBracket` 📖	CompOp	—
`addCommGroup` 📖	CompOp	15 math math: `mk_eq_zero`, `mk'_ker`, `toEnd_comp_mk'`, `range_mk'`, `coe_lowerCentralSeries_ideal_quot_eq`, `LieModule.isNilpotent_quotient_iff`, `map_mk'_eq_bot_le`, `isCentralScalar`, `surjective_mk'`, `lieModuleHom_ext_iff`, `mk_eq_zero'`, `LieSubalgebra.normalizer_eq_self_iff`, `lieQuotientLieModule`, `isNoetherian`, `mk'_apply`
`inhabited` 📖	CompOp	—
`lieQuotientHasBracket` 📖	CompOp	1 math math: `mk_bracket`
`lieQuotientLieAlgebra` 📖	CompOp	3 math math: `LieHom.quotKerEquivRange_toFun`, `coe_lowerCentralSeries_ideal_quot_eq`, `LieHom.quotKerEquivRange_invFun`
`lieQuotientLieRing` 📖	CompOp	3 math math: `LieHom.quotKerEquivRange_toFun`, `coe_lowerCentralSeries_ideal_quot_eq`, `LieHom.quotKerEquivRange_invFun`
`lieQuotientLieRingModule` 📖	CompOp	12 math math: `mk_eq_zero`, `mk'_ker`, `toEnd_comp_mk'`, `range_mk'`, `coe_lowerCentralSeries_ideal_quot_eq`, `LieModule.isNilpotent_quotient_iff`, `map_mk'_eq_bot_le`, `surjective_mk'`, `lieModuleHom_ext_iff`, `LieSubalgebra.normalizer_eq_self_iff`, `lieQuotientLieModule`, `mk'_apply`
`lieSubmoduleInvariant` 📖	CompOp	—
`mk` 📖	CompOp	—
`mk'` 📖	CompOp	8 math math: `mk_eq_zero`, `mk'_ker`, `toEnd_comp_mk'`, `range_mk'`, `map_mk'_eq_bot_le`, `surjective_mk'`, `lieModuleHom_ext_iff`, `mk'_apply`
`module'` 📖	CompOp	1 math math: `isCentralScalar`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `module'` `MulOpposite` `MulOpposite.instMonoid` `MulOpposite.instSemiring`	—	`Submodule.Quotient.isCentralScalar`
`isNoetherian` 📖	mathematical	—	`IsNoetherian` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `addCommGroup` `module`	—	`isNoetherian_quotient`
`is_quotient_mk` 📖	mathematical	—	`Quotient.mk''` `Submodule.quotientRel` `CommRing.toRing` `LieSubmodule.toSubmodule`	—	—
`lieModuleHom_ext` 📖	—	`LieModuleHom.comp` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `mk'`	—	—	`LieModuleHom.ext` `Quotient.inductionOn'` `LieModuleHom.congr_fun`
`lieModuleHom_ext_iff` 📖	mathematical	—	`LieModuleHom.comp` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `mk'`	—	`lieModuleHom_ext`
`lieQuotientLieModule` 📖	mathematical	—	`LieModule` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule`	—	`LieModule.compLieHom` `smulCommClass_self` `IsScalarTower.left` `Module.End.instLieModule`
`map_mk'_eq_bot_le` 📖	mathematical	—	`LieSubmodule.map` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `mk'` `Bot.bot` `LieSubmodule.instBot` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder`	—	`LieModuleHom.le_ker_iff_map` `mk'_ker`
`mk'_apply` 📖	mathematical	—	`DFunLike.coe` `LieModuleHom` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `LieModuleHom.instFunLike` `mk'`	—	—
`mk'_ker` 📖	mathematical	—	`LieModuleHom.ker` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `mk'`	—	`LieSubmodule.ext`
`mk_bracket` 📖	mathematical	—	`LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `Bracket.bracket` `LieRingModule.toBracket` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `lieQuotientHasBracket`	—	—
`mk_eq_zero` 📖	mathematical	—	`DFunLike.coe` `LieModuleHom` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `LieModuleHom.instFunLike` `mk'` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SetLike.instMembership` `LieSubmodule.instSetLike`	—	`Submodule.Quotient.mk_eq_zero`
`mk_eq_zero'` 📖	mathematical	—	`HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup` `SetLike.instMembership` `LieSubmodule.instSetLike`	—	`Submodule.Quotient.mk_eq_zero`
`range_mk'` 📖	mathematical	—	`LieModuleHom.range` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `addCommGroup` `module` `lieQuotientLieRingModule` `mk'` `Top.top` `LieSubmodule.instTop`	—	—
`surjective_mk'` 📖	mathematical	—	`HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `DFunLike.coe` `LieModuleHom` `addCommGroup` `module` `lieQuotientLieRingModule` `LieModuleHom.instFunLike` `mk'`	—	`Quot.mk_surjective`
`toEnd_comp_mk'` 📖	mathematical	—	`LinearMap.comp` `HasQuotient.Quotient` `LieSubmodule` `LieSubmodule.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `addCommGroup` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `lieQuotientLieRingModule` `lieQuotientLieModule` `LieModuleHom.toLinearMap` `mk'`	—	`RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `lieQuotientLieModule`

---

← Back to Index