inclusion_self

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.inclusion_self

← MathLib Explorer

English

The inclusion of a subalgebra into itself is the identity homomorphism.

Русский

Включение S в S равно тождественному гомоморфизму над S.

LaTeX

$$$\\text{inclusion}_{\\leq}\\;S = \\mathrm{id}_S$$$

Lean4

@[simp]
theorem inclusion_self {S : NonUnitalStarSubalgebra R A} : inclusion (le_refl S) = NonUnitalAlgHom.id R S :=
  NonUnitalAlgHom.ext fun _x => Subtype.ext rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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