fintype

Mathlib.Algebra.Group.TypeTags.Finite

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

English

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

Русский

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

LaTeX

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

Lean4

instance fintype : ∀ [Fintype α], Fintype (Multiplicative α) :=
  Fintype.ofEquiv α Multiplicative.ofAdd

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

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

Разделы

Аффилиация

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