instFinite — Mathlib

English

For any Klein four group G that is finite, the cardinality |G| equals 4.

Русский

Для любой конечной группы G с свойством Klein Four выполняется |G| = 4.

LaTeX

$$|G| = 4$$

Lean4

/-- This instance is scoped, because it always applies (which makes linting and typeclass inference
potentially *a lot* slower). -/
@[to_additive]
scoped instance instFinite {G : Type*} [Group G] [IsKleinFour G] : Finite G :=
  Nat.finite_of_card_ne_zero <| by simp [IsKleinFour.card_four]

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