surj — Mathlib

English

The canonical localization map is surjective.

Русский

Каноническое отображение локализации сюръективно.

LaTeX

$$$$ \mathrm{fromLocalizedModule} \text{ is surjective}. $$$$

Lean4

theorem surj : Function.Surjective <| fromLocalizedModule S f := fun x =>
  let ⟨⟨m, s⟩, eq1⟩ := IsLocalizedModule.surj S f x
  ⟨LocalizedModule.mk m s, by
    rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← eq1, Submonoid.smul_def]⟩

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