inclusion_self

Mathlib.Algebra.Algebra.Subalgebra.Basic

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

English

The inclusion map for the case h = le_refl S is the identity on S.

Русский

Включение при h = ле-рефл S является тождественным на S.

LaTeX

$$$\text{inclusion}(\mathrm{le\_refl}(S)) = \mathrm{AlgHom.id}(R,S)$$$

Lean4

@[simp]
theorem inclusion_self : inclusion (le_refl S) = AlgHom.id R S :=
  AlgHom.ext fun _x => Subtype.ext rfl

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

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

Разделы

Аффилиация

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