finrank_eq_one_iff — Mathlib

English

For a subalgebra S of E with Nontrivial E and S free over F, finrank F S = 1 iff S = ⊥.

Русский

Для подалгебры S ⊆ E, если E нетривиально и S свободно над F, тогда finrank_F S = 1 тогда и только тогда S = ⊥.

LaTeX

$$$\operatorname{finrank} F S = 1 \iff S = ⊥$$$

Lean4

@[simp]
theorem finrank_eq_one_iff [Nontrivial E] [Module.Free F S] : finrank F S = 1 ↔ S = ⊥ :=
  by
  rw [← Subalgebra.rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

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