coe_incl'

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.coe_incl'

English

The coercion of incl' equals the identity on L'.

Русский

Приведение incl' равняется тождественному отображению на L'.

LaTeX

$$$$\text{@[simp]}\ (\text{coe}_{\mathsf{LieModuleHom}}\, L'.incl') = \text{Subtype.val}.$$$$

Lean4

@[simp]
theorem coe_incl' : ⇑L'.incl' = ((↑) : L' → L) :=
  rfl

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

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

Разделы

Аффилиация

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