awayToAwayRight_eq — Mathlib

English

For all a ∈ R, the value of awayToAwayRight x y on algebraMap_R^S(a) equals algebraMap_R^P(a).

Русский

Для любого a ∈ R, значение awayToAwayRight x y на algebraMap_R^S(a) равно algebraMap_R^P(a).

LaTeX

$$$\\text{awayToAwayRight } x\\, y\\big(\\operatorname{algebraMap}_{R,S}(a)\\big) = \\operatorname{algebraMap}_{R,P}(a)$$$

Lean4

theorem awayToAwayRight_eq (y : R) [Algebra R P] [IsLocalization.Away (x * y) P] (a : R) :
    awayToAwayRight x y (algebraMap R S a) = algebraMap R P a :=
  lift_eq _ _ _

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