eq_bot_iff_forall — Mathlib

English

A subgroup equals the bottom subgroup iff every element of it is the identity.

Русский

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

LaTeX

$$$$ H = \\bot \\iff \\forall x \\in H,\ x = 1. $$$$

Lean4

@[to_additive]
theorem eq_bot_iff_forall : H = ⊥ ↔ ∀ x ∈ H, x = (1 : G) :=
  toSubmonoid_injective.eq_iff.symm.trans <| Submonoid.eq_bot_iff_forall _

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