Mathlib Map

Theorems · Theorem · nonassociative algebras

LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra

∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L)
  [H.IsCartanSubalgebra] (k : ℕ), LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
Defined in
Mathlib.Algebra.Lie.CartanSubalgebra
Cited by
1 results in Mathlib
Foundations
Depth 32 from the axioms · uses propext, Quot.sound
Assumes
CommRingLieRingLieAlgebraLieSubalgebra.IsCartanSubalgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit · cited by 0LieSubalgebra.isCartanSub…CommRing · cited by 17173CommRingLieRing · cited by 1548LieRingLieAlgebra · cited by 1246LieAlgebraLieSubmodule · cited by 489LieSubmoduleLieSubalgebra · cited by 418LieSubalgebraLieSubalgebra.IsCartanSubalgebra · cited by 135LieSubalgebra.IsCartanSub…LieSubalgebra.toLieSubmodule · cited by 26LieSubalgebra.toLieSubmod…LieSubmodule.ucs · cited by 21LieSubmodule.ucsLieSubmodule.ucs_succ · cited by 9LieSubmodule.ucs_succLieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra · cited by 3LieSubalgebra.normalizer_…LieSubmodule.normalizer.congr_simp · cited by 2normalizer.congr_simpLieSubalgebra.ucs_eq_self_of_…CITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.