Theorems · Theorem · nonassociative algebras

LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top

∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H),
  iSup ![H.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Lemma 4.5 from [Geck](Geck2017).

Defined in: Mathlib.Algebra.Lie.Basis.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Finite CommRing LieRing LieAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites35

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

CommRingstatement and proof · cited by 17,173
Top.topstatement and proof · cited by 9,680
Set.rangeproof · cited by 4,705
Finitestatement and proof · cited by 3,029
iSupstatement · cited by 2,415
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
Matrix.vecConsstatement · cited by 852
Matrix.vecEmptystatement · cited by 832
Bracket.bracketproof · cited by 642
LieSubmodulestatement · cited by 489
LieSubalgebrastatement and proof · cited by 418

Cited by4

Results whose statement or proof uses this declaration.

LieAlgebra.Basis.cartan_eqproof · cited by 2
LieAlgebra.Basis.borelUpper_eqproof · cited by 1
LieAlgebra.Basis.borelLower_eqproof · cited by 1
LieAlgebra.Basis.root_mem_or_mem_negproof · cited by 0