ext

Mathlib.Algebra.Lie.Submodule

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

English

LieSubmodules N and N' are equal if they have the same elements.

Русский

Подмодули Ли N и N' равны, если совпадают их множества элементов.

LaTeX

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

Lean4

@[ext]
theorem ext (h : ∀ m, m ∈ N ↔ m ∈ N') : N = N' :=
  SetLike.ext h

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

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

Разделы

Аффилиация

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