exists_integer_multiple — Mathlib

English

The localized module LocalizedModule S M is subsingleton if and only if for all m ∈ M there exists r ∈ S with r•m = 0.

Русский

Локализованный модуль LocalizedModule S M одноэлементен тогда и только тогда, когда для каждого m ∈ M существует r ∈ S такое, что r•m = 0.

LaTeX

$$$\operatorname{Subsingleton}(\mathrm{LocalizedModule}\;S\;M) \iff \forall m:\, \exists r \in S, r\cdot m = 0$$$

Lean4

/-- Each element `x : M'` has an `S`-multiple which is an integer. -/
theorem exists_integer_multiple (x : M') : ∃ a : S, IsInteger f (a.val • x) :=
  let ⟨⟨Num, denom⟩, h⟩ := IsLocalizedModule.surj S f x
  ⟨denom, Set.mem_range.mpr ⟨Num, h.symm⟩⟩

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