ringEquivOfRingEquiv — Mathlib

English

The map f ↦ f ∘ algebraMap A K is injective on RingHom K L.

Русский

Отображение f ↦ f ∘ algebraMap A K инъективно на RingHom K L.

LaTeX

$$$\text{Injective } (\lambda f : K \to+* L, f \circ (\operatorname{algebraMap} A K))$$$

Lean4

/-- Given rings `A, B` and localization maps to their fraction rings
`f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces an isomorphism of
fraction rings `K ≃+* L`. -/
noncomputable def ringEquivOfRingEquiv : K ≃+* L :=
  IsLocalization.ringEquivOfRingEquiv K L h (MulEquivClass.map_nonZeroDivisors h)

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