Theorems · Theorem · linear algebra

Subalgebra.eq_of_le_of_finrank_le

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Ring L] [inst_2 : Algebra K L] {F E : Subalgebra K L}
  [hfin : FiniteDimensional K ↥E], F ≤ E → Module.finrank K ↥E ≤ Module.finrank K ↥F → F = E

If a subalgebra is contained in a finite-dimensional subalgebra with the same or smaller dimension, they are equal.

Defined in

Mathlib.LinearAlgebra.FiniteDimensional.Basic

Cited by

2 results in Mathlib

Foundations

Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebraFiniteDimensional