addCommMonoid

Mathlib.Algebra.Group.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.addCommMonoid

← MathLib Explorer

English

For n with NeZero n, Fin(n) carries an AddCommMonoid structure.

Русский

Для n, не равного нулю, Fin(n) имеет структуру AddCommMonoid.

LaTeX

$$$\\operatorname{AddCommMonoid}(\\mathrm{Fin}(n))\\quad(\\text{with } n\\neq 0)$$$

Lean4

instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n)
    where
  zero_add := Fin.zero_add
  add_zero := Fin.add_zero
  nsmul := nsmulRec
  __ := Fin.addCommSemigroup n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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