instIsEmptyOfSubsingleton

Mathlib.Algebra.Lie.Weights.Basic

URI: https://scilib.ai/kg/mathlib#LieModule.Weight.instIsEmptyOfSubsingleton

English

If M is a subsingleton, then the weight object is empty, i.e., Weight R L M has no elements.

Русский

Если M является подселеделом, то весовой объект пуст, то есть Weight R L M не содержит элементов.

LaTeX

$$$\\text{IsEmpty}(\\mathrm{Weight}\\;R\\;L\\;M)$ when $|M| = 1$$$

Lean4

instance [Subsingleton M] : IsEmpty (Weight R L M) :=
  ⟨fun h ↦ h.2 (Subsingleton.elim _ _)⟩

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

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

Разделы

Аффилиация

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