instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup

English

For every natural n, the alternating group on Fin(n+3) is nontrivial.

Русский

Для любого натурального n чередующаяся группа на Fin(n+3) не тривиальна.

LaTeX

$$$$\\forall n \\in \\mathbb{N},\\; \\operatorname{Nontrivial}(\\operatorname{alternatingGroup}(\\operatorname{Fin}(n+3))).$$$$

Lean4

instance {n : ℕ} : Nontrivial (alternatingGroup (Fin (n + 3))) :=
  nontrivial_of_three_le_card
    (by
      rw [card_fin]
      exact le_add_left (le_refl 3))

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