fintype

Mathlib.Algebra.Group.TypeTags.Finite

URI: https://scilib.ai/kg/mathlib#Additive.fintype

English

There is a finite-type equivalence between α and Additive α given a finite type on α.

Русский

Существует эквивалентность между типами α и Additive α при условии, что α конечен.

LaTeX

$$$\text{Additive.fintype}$ : ∀ [Fintype α], Fintype (Additive α)$$

Lean4

instance fintype : ∀ [Fintype α], Fintype (Additive α) :=
  Fintype.ofEquiv α Additive.ofMul

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

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

Разделы

Аффилиация

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