instNeZeroNatCardOfNonempty

Mathlib.Data.Fintype.Card

URI: https://scilib.ai/kg/mathlib#Fintype.instNeZeroNatCardOfNonempty

English

For nonempty α, NeZero (card α).

Русский

Для непустого α имеет место NeZero(card α).

LaTeX

$$Nonempty(\alpha) \Rightarrow NeZero(|\alpha|)$$

Lean4

instance [Nonempty α] : NeZero (card α) :=
  ⟨card_ne_zero⟩

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

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

Разделы

Аффилиация

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