of_le_of_exists_dvd — Mathlib

English

If every element of N divides some element of M, then N localizes to S.

Русский

Если каждый элемент из N делится на некоторый элемент из M, то N локализуется в S.

LaTeX

$$$\\text{IsLocalization } N S$ при условии: \\forall n\\in N, \\exists m\\in M, n \\mid m$$

Lean4

theorem of_le_of_exists_dvd (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) : IsLocalization N S :=
  of_le M N h₁ fun n hn ↦
    have ⟨m, hm, dvd⟩ := h₂ n hn
    isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)

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