instFiniteUnits

Mathlib.Data.Fintype.Units

URI: https://scilib.ai/kg/mathlib#instFiniteUnits

English

If α is a finite, monoid, then the set of units αˣ is finite.

Русский

Если α моноид конечен, то множество едениц αˣ конечно.

LaTeX

$$$$\\text{Finite}(\\mathrm{Units}(\\alpha)).$$$$

Lean4

instance [Monoid α] [Finite α] : Finite αˣ :=
  .of_injective _ Units.val_injective

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

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

Разделы

Аффилиация

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