theorem LieSubalgebra.finrank_congr {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {p q : LieSubalgebra R L} (h : p = q) : Module.finrank R ↥p = Module.finrank R ↥q

theorem LieIdeal.finrank_congr {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {p q : LieIdeal R L} (h : p = q) : Module.finrank R ↥p = Module.finrank R ↥q

@[simp]

theorem LieIdeal.finrank_toLieSubalgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (p : LieIdeal R L) : Module.finrank R ↥(toLieSubalgebra R L p) = Module.finrank R ↥p

@[simp]

theorem LieIdeal.finrank_toSubmodule {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (p : LieIdeal R L) : Module.finrank R ↥↑p = Module.finrank R ↥p

theorem LieIdeal.finrank_lt_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {p : LieIdeal K L} : Module.finrank K ↥p < Module.finrank K L ↔ p < ⊤

@[simp]

theorem LieIdeal.finrank_top {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : Module.finrank R ↥⊤ = Module.finrank R L

@[simp]

theorem LieIdeal.finrank_lieIdealOf {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (p q : LieIdeal R L) (h : p ≤ q) : Module.finrank R ↥(p.lieIdealOf q) = Module.finrank R ↥p

@[simp]

theorem LieIdeal.finrank_quotient_toSubmodule {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (p : LieIdeal R L) : Module.finrank R (L ⧸ ↑p) = Module.finrank R (L ⧸ p)

@[simp]

theorem LieIdeal.finrank_quotient {R : Type u_1} {L : Type u} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial R] [HasRankNullity.{u, u_1} R] [Module.Finite R L] (p : LieIdeal R L) : Module.finrank R (L ⧸ p) = Module.finrank R L - Module.finrank R ↥p

@[simp]

theorem LieIdeal.finrank_le {R : Type u_1} {L : Type u} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial R] [HasRankNullity.{u, u_1} R] [Module.Finite R L] (p : LieIdeal R L) : Module.finrank R ↥p ≤ Module.finrank R L

theorem LieHom.finrank_range_add_finrank_ker {K : Type u_1} {L : Type u_2} {L₂ : Type u_3} [Field K] [LieRing L] [LieAlgebra K L] [LieRing L₂] [LieAlgebra K L₂] [FiniteDimensional K L] (f : L →ₗ⁅K⁆ L₂) : Module.finrank K ↥f.range + Module.finrank K ↥f.ker = Module.finrank K L

theorem LieHom.finrank_idealRange_add_finrank_ker {K : Type u_1} {L : Type u_2} {L₂ : Type u_3} [Field K] [LieRing L] [LieAlgebra K L] [LieRing L₂] [LieAlgebra K L₂] [FiniteDimensional K L] (f : L →ₗ⁅K⁆ L₂) (hf : f.IsIdealMorphism) : Module.finrank K ↥f.idealRange + Module.finrank K ↥f.ker = Module.finrank K L