nontrivial_iff_ne_bot — Mathlib

English

A subgroup is nontrivial iff it is not equal to the bottom subgroup.

Русский

Подгруппа не тривиальна тогда и только тогда, когда она не равна нижней подгруппе.

LaTeX

$$$$ \\mathrm{Nontrivial}(H) \\iff H \\neq \\bot. $$$$

Lean4

@[to_additive]
theorem nontrivial_iff_ne_bot (H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥ :=
  by
  rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
  simp only [ne_eq, not_forall, exists_prop]

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