mk_smul_mk_quotient_map_quotient — Mathlib

English

There is an IsScalarTower structure: IsScalarTower R (R ⧸ p) (S ⧸ map (algebraMap R S) p).

Русский

Существует структура IsScalarTower: R → (R ⧸ p) → (S ⧸ map (algebraMap R S) p).

LaTeX

$$$\\text{IsScalarTower } R (R / p) (S / map (algebraMap R S) p)$$$

Lean4

@[simp]
theorem mk_smul_mk_quotient_map_quotient (x : R) (y : S) :
    letI f := algebraMap R S
    Quotient.mk p x • Quotient.mk (map f p) y = Quotient.mk (map f p) (f x * y) :=
  Algebra.smul_def _ _

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