eq_of_le_of_finrank_le — Mathlib

English

If F ≤ E are subalgebras contained in a finite-dimensional ambient algebra E with finrank_K E ≤ finrank_K F, then F = E.

Русский

Если подалгебра F ⊆ E и E — конечномерна над K, и dim E ≤ dim F, то F = E.

LaTeX

$$$[\operatorname{FiniteDimensional}_K E] \Rightarrow (F \le E \Rightarrow \operatorname{finrank}_K E \le \operatorname{finrank}_K F \Rightarrow F = E)$$$

Lean4

/-- If a subalgebra is contained in a finite-dimensional
subalgebra with the same or smaller dimension, they are equal. -/
theorem eq_of_le_of_finrank_le (h_le : F ≤ E) (h_finrank : finrank K E ≤ finrank K F) : F = E :=
  haveI : Module.Finite K (Subalgebra.toSubmodule E) := hfin
  toSubmodule_injective <| Submodule.eq_of_le_of_finrank_le h_le h_finrank

Похожие утверждения