away_snd — Mathlib

English

Similarly, the localization away from (0,1) in R × S is canonically isomorphic to S.

Русский

Аналогично, локализация away от (0,1) в R × S естественно изоморфна S.

LaTeX

$$$\text{Away } (0,1) \; \text{ on } R \times S \cong S$$$

Lean4

instance away_snd {R S} [CommSemiring R] [CommSemiring S] :
    letI := (RingHom.snd R S).toAlgebra
    IsLocalization.Away (R := R × S) (0, 1) S :=
  letI := (RingHom.snd R S).toAlgebra
  away_of_isIdempotentElem_of_mul (by ext <;> simp) (fun ⟨xR, xS⟩ ⟨yR, yS⟩ ↦ show xS = yS ↔ _ by simp)
    Prod.snd_surjective

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