English
Module.Finite for Finsupp ι M holds iff either ι is empty, or M is a subsingleton, or both M is finite and ι finite.
Русский
Module.Finite для Finsupp ι M эквивалентно: либо ι пусто, либо M — подсинглтон, либо оба условия: M конечен и ι конечен.
LaTeX
$$$$\\\\operatorname{Module.Finite}_R(\\\\text{Finsupp}_{\\\\iota} M) \\\\iff \\\\bigl(\\\\IsEmpty(\\\\iota) \\\\lor \\\\operatorname{Subsingleton} M \\\\lor (\\\\operatorname{Module.Finite}_R M \\\\land \\\\ Finite \\\\iota)\\\\bigr).$$$$
Lean4
@[simp]
theorem finite_finsupp_iff : Module.Finite R (ι →₀ M) ↔ IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι
where
mp := by
simp only [or_iff_not_imp_left, not_subsingleton_iff_nontrivial, not_isEmpty_iff]
rintro h ⟨i⟩ _
obtain ⟨s, hs⟩ := id h
exact
⟨.of_surjective (Finsupp.lapply (R := R) (M := M) i) (Finsupp.apply_surjective i),
finite_of_span_finite_eq_top_finsupp s.finite_toSet hs⟩
mpr
| .inl _ => inferInstance
| .inr <| .inl h => inferInstance
| .inr <| .inr h => by cases h; infer_instance
