Documentation Verification Report

Normalizer

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

Statistics

Metric	Count
Definitions `normalizer`, `idealizer`, `normalizer`	3
Theorems `idealizer_eq_normalizer`, `coe_normalizer_eq_normalizer`, `exists_nested_lieIdeal_ofLe_normalizer`, `ideal_in_normalizer`, `le_normalizer`, `lie_mem_sup_of_mem_normalizer`, `mem_normalizer_iff`, `mem_normalizer_iff'`, `normalizer_eq_self_iff`, `comap_normalizer`, `gc_top_lie_normalizer`, `le_normalizer`, `mem_idealizer`, `mem_normalizer`, `monotone_normalizer`, `normalizer_bot_eq_maxTrivSubmodule`, `normalizer_inf`, `normalizer_mono`, `top_lie_le_iff_le_normalizer`	19
Total	22

LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`idealizer_eq_normalizer` 📖	mathematical	—	`LieSubmodule.idealizer` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieSubmodule.normalizer`	—	`LieSubmodule.ext` `lieAlgebraSelfModule` `lie_skew` `AddSubgroupClass.toNegMemClass` `LieSubmodule.instAddSubgroupClass`

LieSubalgebra

Definitions

Name	Category	Theorems
`normalizer` 📖	CompOp	10 math math: `le_normalizer`, `normalizer_engel`, `coe_normalizer_eq_normalizer`, `normalizer_eq_self_of_engel_le`, `mem_normalizer_iff'`, `IsCartanSubalgebra.self_normalizing`, `LieAlgebra.zeroRootSubalgebra_normalizer_eq_self`, `normalizer_eq_self_iff`, `LieIdeal.normalizer_eq_top`, `mem_normalizer_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_normalizer_eq_normalizer` 📖	mathematical	—	`LieSubmodule.toSubmodule` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingModule` `lieRingSelfModule` `LieSubmodule.normalizer` `lieAlgebra` `lieModule` `lieAlgebraSelfModule` `toLieSubmodule` `toSubmodule` `normalizer`	—	`lieModule` `lieAlgebraSelfModule`
`exists_nested_lieIdeal_ofLe_normalizer` 📖	mathematical	`LieSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder_1` `normalizer`	`LieIdeal` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `lieRing` `lieAlgebra` `LieIdeal.toLieSubalgebra` `ofLe`	—	`exists_nested_lieIdeal_coe_eq_iff` `ideal_in_normalizer`
`ideal_in_normalizer` 📖	mathematical	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `normalizer`	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	`lie_skew` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass`
`le_normalizer` 📖	mathematical	—	`LieSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder_1` `normalizer`	—	`LieSubmodule.le_normalizer` `lieModule` `lieAlgebraSelfModule`
`lie_mem_sup_of_mem_normalizer` 📖	mathematical	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `normalizer` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `Submodule.setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `toSubmodule`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `SetLike.instMembership` `Submodule.setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `toSubmodule` `Bracket.bracket` `LieRingModule.toBracket` `lieRingSelfModule`	—	`Submodule.mem_sup` `Submodule.mem_span_singleton` `Submodule.mem_sup_right` `lie_add` `lie_smul` `lieAlgebraSelfModule` `add_lie` `smul_lie` `lie_self` `smul_zero` `zero_add` `add_mem` `smul_mem` `mem_normalizer_iff'` `mem_normalizer_iff` `lie_mem`
`mem_normalizer_iff` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `normalizer` `Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	`mem_normalizer_iff'` `lie_skew` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass`
`mem_normalizer_iff'` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `normalizer` `Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	`Subtype.forall'`
`normalizer_eq_self_iff` 📖	mathematical	—	`normalizer` `LieModule.maxTrivSubmodule` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `HasQuotient.Quotient` `LieSubmodule` `lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingModule` `lieRingSelfModule` `LieSubmodule.instHasQuotient` `toLieSubmodule` `lieAlgebra` `LieSubmodule.Quotient.addCommGroup` `LieSubmodule.Quotient.module` `LieSubmodule.Quotient.lieQuotientLieRingModule` `lieModule` `lieAlgebraSelfModule` `LieSubmodule.Quotient.lieQuotientLieModule` `Bot.bot` `LieSubmodule.instBot`	—	`lieModule` `lieAlgebraSelfModule` `LieSubmodule.Quotient.lieQuotientLieModule` `LieSubmodule.eq_bot_iff` `mem_normalizer_iff'` `LieSubmodule.Quotient.mk_eq_zero` `LieModuleHom.map_lie` `Submodule.Quotient.mk_eq_zero` `coe_toLieSubmodule` `mem_toSubmodule` `le_antisymm` `coe_bracket_of_module` `mem_toLieSubmodule` `le_normalizer`

LieSubmodule

Definitions

Name	Category	Theorems
`idealizer` 📖	CompOp	2 math math: `mem_idealizer`, `LieIdeal.idealizer_eq_normalizer`
`normalizer` 📖	CompOp	14 math math: `LieSubalgebra.coe_normalizer_eq_normalizer`, `monotone_normalizer`, `ucs_succ`, `top_lie_le_iff_le_normalizer`, `normalizer_inf`, `LieModule.genWeightSpace_zero_normalizer_eq_self`, `normalizer_mono`, `le_normalizer`, `comap_normalizer`, `mem_normalizer`, `normalizer_bot_eq_maxTrivSubmodule`, `LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra`, `LieIdeal.idealizer_eq_normalizer`, `gc_top_lie_normalizer`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_normalizer` 📖	mathematical	—	`comap` `normalizer`	—	`ext` `LieModuleHom.map_lie`
`gc_top_lie_normalizer` 📖	mathematical	—	`GaloisConnection` `LieSubmodule` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `LieIdeal` `hasBracket` `Top.top` `instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `normalizer`	—	`top_lie_le_iff_le_normalizer`
`le_normalizer` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	—	`mem_normalizer` `lie_mem`
`mem_idealizer` 📖	mathematical	—	`LieIdeal` `SetLike.instMembership` `instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `idealizer` `LieSubmodule` `Bracket.bracket` `LieRingModule.toBracket`	—	—
`mem_normalizer` 📖	mathematical	—	`LieSubmodule` `SetLike.instMembership` `instSetLike` `normalizer` `Bracket.bracket` `LieRingModule.toBracket`	—	—
`monotone_normalizer` 📖	mathematical	—	`Monotone` `LieSubmodule` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	—	`normalizer_mono`
`normalizer_bot_eq_maxTrivSubmodule` 📖	mathematical	—	`normalizer` `Bot.bot` `LieSubmodule` `instBot` `LieModule.maxTrivSubmodule`	—	—
`normalizer_inf` 📖	mathematical	—	`normalizer` `LieSubmodule` `instMin`	—	`ext`
`normalizer_mono` 📖	mathematical	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	—	`mem_normalizer`
`top_lie_le_iff_le_normalizer` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `LieIdeal` `hasBracket` `Top.top` `instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `normalizer`	—	`lie_le_iff`

---

← Back to Index