bot_eq_top_iff_rank_eq_one — Mathlib

English

For a nontrivial E with E free over F, bottom equals top if and only if the rank of E over F is 1.

Русский

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

LaTeX

$$(⊥ = ⊤) ↔ rank_F E = 1$$

Lean4

theorem bot_eq_top_iff_rank_eq_one [Nontrivial E] [Module.Free F E] : (⊥ : Subalgebra F E) = ⊤ ↔ Module.rank F E = 1 :=
  by
  haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]

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