exists_integer_multiple' — Mathlib

English

For any a in S there exists b in M such that a * algebraMap(R S) b is an integer.

Русский

Для любого a в S существует b в M, такое что a • algebraMap(R S) b целое.

LaTeX

$$exists_integer_multiple'(a)$$

Lean4

/-- Each element `a : S` has an `M`-multiple which is an integer.

This version multiplies `a` on the right, matching the argument order in `LocalizationMap.surj`.
-/
theorem exists_integer_multiple' (a : S) : ∃ b : M, IsInteger R (a * algebraMap R S b) :=
  let ⟨⟨Num, denom⟩, h⟩ := IsLocalization.surj _ a
  ⟨denom, Set.mem_range.mpr ⟨Num, h.symm⟩⟩

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