map_eq_self — Mathlib

English

The algebra map from R to itself acts as the identity on all elements: for every x ∈ R, algebraMap R R x = x.

Русский

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

LaTeX

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

Lean4

@[deprecated algebraMap_self_apply (since := "2025-07-17")]
theorem map_eq_self (x : R) : algebraMap R R x = x :=
  rfl

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