finite_finsupp_self_iff — Mathlib

English

Module.Finite for Finsupp ι R is equivalent to Subsingleton R or Finite ι.

Русский

Module.Finite для Finsupp ι R эквивалентно Subsingleton R или Finite ι.

LaTeX

$$$$\\\\operatorname{Module.Finite}_R(\\\\iota \\\\to_0 R) \\\\iff \\\\operatorname{Subsingleton} R \\\\lor \\\\operatorname{Finite} \\\\iota.$$$$

Lean4

@[simp high]
theorem finite_finsupp_self_iff : Module.Finite R (ι →₀ R) ↔ Subsingleton R ∨ Finite ι :=
  by
  simp only [finite_finsupp_iff, Finite.self, true_and, or_iff_right_iff_imp]
  exact fun _ ↦ .inr inferInstance

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