away_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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