fintypePowers

Mathlib.Algebra.Group.Submonoid.Membership

URI: https://scilib.ai/kg/mathlib#Submonoid.fintypePowers

English

If M is finite, then powers(a) is finite.

Русский

Если множество M конечно, то powers(a) конечно.

LaTeX

$$[Fintype M] ⇒ Fintype (powers(a))$$

Lean4

noncomputable instance fintypePowers [Fintype M] : Fintype (powers a) :=
  inferInstanceAs <| Fintype { y // y ∈ powers a }

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

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

Разделы

Аффилиация

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