id

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#StarAlgHom.id

English

The underlying function of the identity star-algebra homomorphism is the identity function.

Русский

Базовая функция идентичности звездно-алгебра-гомоморфизма равна функции-идентичности.

LaTeX

$$$\mathrm{coeff}(\mathrm{id}) = \mathrm{id}$$$

Lean4

/-- The identity as a `StarAlgHom`. -/
protected def id : A →⋆ₐ[R] A :=
  { AlgHom.id _ _ with map_star' := fun _ => rfl }

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

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

Разделы

Аффилиация

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