localization_map_bijective — Mathlib

English

In the field case, localizing at a submonoid not containing 0 induces no new elements; the localization map is bijective.

Русский

В случае поля локализация по подмоноиду, не содержащему 0, не порождает новых элементов; локализационная карта биективна.

LaTeX

$$$\text{Field.local localization bijection}$$$

Lean4

/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
theorem localization_map_bijective {K Kₘ : Type*} [Field K] [CommRing Kₘ] {M : Submonoid K} (hM : (0 : K) ∉ M)
    [Algebra K Kₘ] [IsLocalization M Kₘ] : Function.Bijective (algebraMap K Kₘ) :=
  (Field.toIsField K).localization_map_bijective hM

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