nontrivial_iff_exists_ne_one — Mathlib

English

A subgroup is nontrivial iff it contains an element different from the identity.

Русский

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

LaTeX

$$$$ \\mathrm{Nontrivial}(H) \\iff \\exists x \\in H, x \\neq 1. $$$$

Lean4

@[to_additive]
theorem nontrivial_iff_exists_ne_one (H : Subgroup G) : Nontrivial H ↔ ∃ x ∈ H, x ≠ (1 : G) :=
  by
  rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
  simp

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