bot_lt_center — Mathlib

English

From center nontrivial, the bottom is strictly less than center in the lattice of subgroups.

Русский

Из ненулевого центра следует, что нижний элемент строго меньше центра в декартовой решётке подгрупп.

LaTeX

$$$[Nontrivial G] [Finite G] \rightarrow \bot < Subgroup.center G$$$

Lean4

theorem bot_lt_center [Nontrivial G] [Finite G] : ⊥ < Subgroup.center G :=
  by
  haveI := center_nontrivial hG
  classical exact bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

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