ringEquivOfRingEquiv_eq — Mathlib

English

For any x in R, the localization isomorphism sends algebra_map(x) to algebra_map(j x) in the target localization.

Русский

Для любого x ∈ R локализационная изоморфизм отображает algebra_map(x) в algebra_map(j x) в целевой локализации.

LaTeX

$$$$ \\mathrm{ringEquivOfRingEquiv}(S,Q,j,H)(\\mathrm{algebraMap}_{R\\to S}(x)) = \\mathrm{algebraMap}_{P\\to Q}(j x) $$$$

Lean4

theorem ringEquivOfRingEquiv_eq {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x) :
    ringEquivOfRingEquiv S Q j H ((algebraMap R S) x) = algebraMap P Q (j x) := by simp

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