algebraMap_apply — Mathlib

English

If S1 is an R-algebra, then applying algebraMap to an element r ∈ R equals applying algebraMap to r in S1 and then embedding via C.

Русский

Если S1 — алгебра над R, то применение algebraMap к элементу r ∈ R равно применению algebraMap к r в S1 и последующему внедрению через C.

LaTeX

$$$ [Algebra\ R\ S_1] (r) : algebraMap\ R (MvPolynomial(σ,S_1))\, r = C( algebraMap\ R S_1\, r ) $$$

Lean4

@[simp]
theorem algebraMap_apply [Algebra R S₁] (r : R) : algebraMap R (MvPolynomial σ S₁) r = C (algebraMap R S₁ r) :=
  rfl

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