constRingHom_eq_algebraMap — Mathlib

English

The constant AlgHom from R to A → R coincides with algebra_of_id, i.e., the natural embedding of R into A → R.

Русский

Константный AlgHom из R в A → R совпадает с Algebra.ofId, т.е. естественным вложением R в A → R.

LaTeX

$$$ constAlgHom R A R = Algebra.ofId R (A \\to R) $$$

Lean4

/-- When `R` is commutative and permits an `algebraMap`, `Pi.constRingHom` is equal to that
map. -/
@[simp]
theorem constRingHom_eq_algebraMap : constRingHom A R = algebraMap R (A → R) :=
  rfl

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