instUniqueSubtypeMemBot

Mathlib.Algebra.Group.Subgroup.Lattice

URI: https://scilib.ai/kg/mathlib#Subgroup.instUniqueSubtypeMemBot

English

There is a unique element of the bottom subtype, namely 1.

Русский

Существует единственный элемент типа подмножества, равный 1.

LaTeX

$$$$ \\text{There is a unique element of } (\\bot : \\mathrm{Subgroup}(G)) \\text{, namely } 1. $$$$

Lean4

@[to_additive]
instance : Unique (⊥ : Subgroup G) :=
  ⟨⟨1⟩, fun g => Subtype.ext g.2⟩

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

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

Разделы

Аффилиация

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