inclusion_self — Mathlib

English

The inclusion map sends an element of a subalgebra S into the ambient A by simply taking its underlying value, preserving membership.

Русский

Включение отображает элемент из подпалгебры S в окружающий A по его базовому значению, сохраняя принадлежность.

LaTeX

$$coe_inclusion : (inclusion h s) = s$$

Lean4

@[simp]
theorem inclusion_self {S : NonUnitalSubalgebra R A} : inclusion (le_refl S) = NonUnitalAlgHom.id R S :=
  rfl

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