Documentation Verification Report

CartanSubalgebra

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

Statistics

Metric	Count
Definitions `IsCartanSubalgebra`, `IsUcsLimit`	2
Theorems `top_isCartanSubalgebra_of_nilpotent`, `normalizer_eq_top`, `nilpotent`, `self_normalizing`, `instIsNilpotentSubtypeMemOfIsCartanSubalgebra`, `instNontrivialSubtypeMemOfIsCartanSubalgebra`, `isCartanSubalgebra_iff_isUcsLimit`, `ne_bot_of_isCartanSubalgebra`, `normalizer_eq_self_of_isCartanSubalgebra`, `ucs_eq_self_of_isCartanSubalgebra`	10
Total	12

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`top_isCartanSubalgebra_of_nilpotent` 📖	mathematical	—	`LieSubalgebra.IsCartanSubalgebra` `Top.top` `LieSubalgebra` `LieSubalgebra.instTop`	—	`instIsNilpotentSubtypeMemLieSubalgebraTop` `LieIdeal.top_toLieSubalgebra` `LieIdeal.normalizer_eq_top`

LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalizer_eq_top` 📖	mathematical	—	`LieSubalgebra.normalizer` `toLieSubalgebra` `Top.top` `LieSubalgebra` `LieSubalgebra.instTop`	—	`LieSubalgebra.ext` `LieSubmodule.lie_mem`

LieSubalgebra

Definitions

Name	Category	Theorems
`IsCartanSubalgebra` 📖	CompData	6 math math: `LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_card`, `LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq`, `LieAlgebra.exists_isCartanSubalgebra_engel`, `LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan`, `isCartanSubalgebra_iff_isUcsLimit`, `LieAlgebra.top_isCartanSubalgebra_of_nilpotent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsNilpotentSubtypeMemOfIsCartanSubalgebra` 📖	mathematical	—	`LieRing.IsNilpotent` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `lieRing`	—	`IsCartanSubalgebra.nilpotent`
`instNontrivialSubtypeMemOfIsCartanSubalgebra` 📖	mathematical	—	`Nontrivial` `LieSubalgebra` `SetLike.instMembership` `instSetLike`	—	`subsingleton_or_nontrivial` `ne_bot_of_isCartanSubalgebra` `eq_bot_iff` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`isCartanSubalgebra_iff_isUcsLimit` 📖	mathematical	—	`IsCartanSubalgebra` `LieSubmodule.IsUcsLimit` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `lieRing` `lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingModule` `lieRingSelfModule` `lieModule` `lieAlgebraSelfModule` `toLieSubmodule`	—	`lieModule` `lieAlgebraSelfModule` `instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.isNilpotent_iff_exists_self_le_ucs` `le_antisymm` `LieSubmodule.ucs_le_of_normalizer_eq_self` `normalizer_eq_self_of_isCartanSubalgebra` `LieSubmodule.ucs_add` `ucs_eq_self_of_isCartanSubalgebra` `LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot` `eq_bot_iff` `LieSubmodule.lcs_le_iff` `le_refl` `coe_normalizer_eq_normalizer` `LieSubmodule.ucs_succ` `coe_toLieSubmodule`
`ne_bot_of_isCartanSubalgebra` 📖	—	—	—	—	`exists_ne` `lie_zero` `IsCartanSubalgebra.self_normalizing`
`normalizer_eq_self_of_isCartanSubalgebra` 📖	mathematical	—	`LieSubmodule.normalizer` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `lieRing` `lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingModule` `lieRingSelfModule` `lieModule` `lieAlgebraSelfModule` `toLieSubmodule`	—	`lieModule` `lieAlgebraSelfModule` `coe_normalizer_eq_normalizer` `IsCartanSubalgebra.self_normalizing` `coe_toLieSubmodule`
`ucs_eq_self_of_isCartanSubalgebra` 📖	mathematical	—	`LieSubmodule.ucs` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `lieRing` `lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingModule` `lieRingSelfModule` `lieModule` `lieAlgebraSelfModule` `toLieSubmodule`	—	`lieModule` `lieAlgebraSelfModule` `LieSubmodule.ucs_succ` `LieSubmodule.normalizer.congr_simp` `normalizer_eq_self_of_isCartanSubalgebra`

LieSubalgebra.IsCartanSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nilpotent` 📖	mathematical	—	`LieRing.IsNilpotent` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing`	—	—
`self_normalizing` 📖	mathematical	—	`LieSubalgebra.normalizer`	—	—

LieSubmodule

Definitions

Name	Category	Theorems
`IsUcsLimit` 📖	MathDef	1 math math: `LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit`

---

← Back to Index