algebraMap_self_apply — Mathlib

English

Let R be a commutative semiring. The algebra map from R to itself is the identity on R: for every x ∈ R, algebraMap R R x = x.

Русский

Пусть R — коммутативное полугруппа; алгебраическое отображение из R в R есть тождественный отображатель: для каждого x ∈ R выполняется algebraMap R R x = x.

LaTeX

$$$\\forall x \\in R,\\; (\\mathrm{algebraMap}\\; R\\; R)(x) = x$$$

Lean4

theorem algebraMap_self_apply (x : R) : algebraMap R R x = x :=
  rfl

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