bot_eq_top_iff_finrank_eq_one — Mathlib

English

For a nontrivial E with E free over F, bottom equals top if and only if finrank F E = 1.

Русский

Для нетривиального E, свободного над F, нижняя грань равна верхней тогда и только тогда, когда finrank_F E = 1.

LaTeX

$$(⊥ = ⊤) ↔ finrank F E = 1$$

Lean4

theorem bot_eq_top_iff_finrank_eq_one [Nontrivial E] [Module.Free F E] : (⊥ : Subalgebra F E) = ⊤ ↔ finrank F E = 1 :=
  by
  haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank, Subalgebra.finrank_eq_one_iff, eq_comm]

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