ne_bot_iff_exists_ne_one — Mathlib

English

A subgroup is not the bottom subgroup iff it contains a non-identity element as an element of itself.

Русский

Подгруппа не является нижней эквивалентно тому, что в ней есть элемент, отличный от единицы.

LaTeX

$$$$ H \\neq \\bot \\iff \\exists a : \\uparrow H, a \\neq 1. $$$$

Lean4

@[to_additive]
theorem ne_bot_iff_exists_ne_one {H : Subgroup G} : H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1 :=
  by
  rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
  simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]

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