theorem LieEquiv.finrank_eq {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : Module.finrank R L = Module.finrank R L₂

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

@[simp]

theorem LieSubalgebra.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 LieSubmodule.finrank_toSubmodule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : Module.finrank R ↥↑N = Module.finrank R ↥N

@[simp]

theorem LieSubmodule.finrank_quotient_toSubmodule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : Module.finrank R (M ⧸ ↑N) = Module.finrank R (M ⧸ N)

@[simp]

theorem LieSubmodule.finrank_quotient {R : Type u_1} {L : Type u_2} {M : Type u} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [Nontrivial R] [HasRankNullity.{u, u_1} R] [Module.Finite R M] (N : LieSubmodule R L M) : Module.finrank R (M ⧸ N) = Module.finrank R M - Module.finrank R ↥N

@[simp]

theorem LieSubmodule.finrank_le {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [Nontrivial R] [Module.Finite R M] (p : LieSubmodule R L M) : Module.finrank R ↥p ≤ Module.finrank R M

theorem LieSubmodule.eq_top_iff_finrank_eq {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [Module.Finite K V] {W : LieSubmodule K L V} : W = ⊤ ↔ Module.finrank K ↥W = Module.finrank K V

theorem LieSubmodule.finrank_lt_iff {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [Module.Finite K V] {W : LieSubmodule K L V} : Module.finrank K ↥W < Module.finrank K V ↔ W < ⊤

theorem LieSubmodule.finrank_add_eq_of_isCompl {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [LieRingModule L V] {W₁ W₂ : LieSubmodule K L V} (h : IsCompl W₁ W₂) : Module.finrank K ↥W₁ + Module.finrank K ↥W₂ = Module.finrank K V

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 ↥(↑R L p) = Module.finrank R ↥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

theorem LieIdeal.finrank_mono {R : Type u_1} {L : Type u} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial R] {I J : LieIdeal R L} [Module.Finite R ↥J] (hIJ : I ≤ J) : Module.finrank R ↥I ≤ Module.finrank R ↥J

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