ofId

Mathlib.Algebra.Algebra.Hom

URI: https://scilib.ai/kg/mathlib#Algebra.ofId

English

The canonical algebra map from a ring to itself is the identity endomorphism.

Русский

Каноническое алгебраическое отображение из кольца в себя есть тождественный эндоморфизм.

LaTeX

$$$ \\mathrm{ofId}\\;R\\;R = \\mathrm{id}_{R} $$$

Lean4

/-- `AlgebraMap` as an `AlgHom`. -/
def ofId : R →ₐ[R] A :=
  { algebraMap R A with commutes' := fun _ => rfl }

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru