tower_quotient_map_quotient — Mathlib

English

For x ∈ R and y ∈ S, in the quotients we have Quotient.mk p x • Quotient.mk (map p) y = Quotient.mk (map p) (f x * y).

Русский

Для x ∈ R и y ∈ S верно: кадр Quotient.mk p x • Quotient.mk (map p) y = Quotient.mk (map p) (f x · y).

LaTeX

$$$\\operatorname{Quotient.mk} p x \\cdot \\operatorname{Quotient.mk} (map p) y = \\operatorname{Quotient.mk} (map p) (f x \\cdot y)$$$

Lean4

instance tower_quotient_map_quotient [Algebra R S] : IsScalarTower R (R ⧸ p) (S ⧸ map (algebraMap R S) p) :=
  IsScalarTower.of_algebraMap_eq fun x => by
    rw [Quotient.algebraMap_eq, Quotient.algebraMap_quotient_map_quotient, Quotient.mk_algebraMap]

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