coe_sub

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.coe_sub

English

Extensionality principle for LieSubmodules: equality is determined by membership.

Русский

Принцип экстенсиональности для подмодулей Ли: равенство определяется по членству.

LaTeX

$$theorem ext (h : ∀ m, m ∈ N ↔ m ∈ N') : N = N'$$

Lean4

@[simp, norm_cast]
theorem coe_sub (m m' : N) : (↑(m - m') : M) = (m : M) - (m' : M) :=
  rfl

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

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

Разделы

Аффилиация

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