awayToAwayLeft_eq — Mathlib

English

For all y ∈ R, and a ∈ R, the value of awayToAwayLeft x y on algebraMap_R^S(a) equals algebraMap_R^P(a) after applying the target map.

Русский

Для любого y ∈ R и a ∈ R, значение awayToAwayLeft x y на algebraMap_R^S(a) равно algebraMap_R^P(a) после применения целевой карты.

LaTeX

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

Lean4

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

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