instBot

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.instBot

English

The bottom element of Associates M is identified with the unit 1.

Русский

Нижний элемент в Associates(M) совпадает с единицей 1.

LaTeX

$$$ \bot = 1 $$$

Lean4

instance [Monoid M] : Bot (Associates M) :=
  ⟨1⟩

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

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

Разделы

Аффилиация

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