finrank_eq_one — Mathlib

English

If σ is empty, then MvPolynomial(σ,K) is canonically isomorphic to K, hence its finite rank is 1.

Русский

Если σ пусто, то MvPolynomial(σ,K) тривиально изоморфна K, следовательно, финитный ранг равен 1.

LaTeX

$$$\\operatorname{Module.finrank}_K\\bigl( \\mathrm{MvPolynomial}(\\sigma,K) \\bigr) = 1$$$

Lean4

theorem finrank_eq_one [IsEmpty σ] : Module.finrank K (MvPolynomial σ K) = 1 :=
  Module.rank_eq_one_iff_finrank_eq_one.mp <| by cases subsingleton_or_nontrivial K <;> simp [rank_eq_lift]

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