coe_val

Mathlib.Algebra.Algebra.Subalgebra.Basic

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

English

The canonical map S.val coincides with the inclusion map into A.

Русский

Каноническое отображение S.val совпадает с включением в A.

LaTeX

$$$S.val = \uparrow$ (inclusion)$$

Lean4

@[simp]
theorem coe_val : (S.val : S → A) = ((↑) : S → A) :=
  rfl

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

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

Разделы

Аффилиация

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