exist_integer_multiples_of_finite

English

The specialized map_exact statement for IsLocalizedModule asserts that if g and h form an exact sequence, then their localized images give an exact sequence after localization.

Русский

Утверждение map_exact для IsLocalizedModule: если g и h образуют точную последовательность, то их локализованные образы также образуют точную последовательность.

LaTeX

$$$\text{Exact}(g,h) \Rightarrow \text{Exact}(\mathrm{map}\;S\;g, \mathrm{map}\;S\;h)$$$

Lean4

/-- We can clear the denominators of a finite indexed family of fractions. -/
theorem exist_integer_multiples_of_finite {ι : Type*} [Finite ι] (g : ι → M') :
    ∃ b : S, ∀ i, IsInteger f ((b : R) • g i) :=
  by
  cases nonempty_fintype ι
  obtain ⟨b, hb⟩ := exist_integer_multiples S f Finset.univ g
  exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩

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