algebraMap_mk' — Mathlib

English

For a in R and s in S, algebraMap R A a under the mk' construction equals mk (algebraMap R A a) s, i.e., the algebra map is transported along mk'.

Русский

Для a в R и s в S алгебраическая карта по mk' даёт mk (algebraMap R A a) s, то есть отображение алгебраической карты переносится вдоль mk'.

LaTeX

$$$\\mathrm{algebraMap}\\_{}(R,A)(a) = \\mathrm{mk}(\\mathrm{algebraMap}\_{R,A}(a), s)$$$

Lean4

theorem algebraMap_mk' {A : Type*} [Semiring A] [Algebra R A] (a : R) (s : S) :
    algebraMap _ _ (IsLocalization.mk' T a s) = mk (algebraMap R A a) s :=
  by
  rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

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