isUnit_iff_singleton_aux — Mathlib

English

In a group, for a finite subset s, the statement “there exists a with s = {a} and IsUnit(a)” is equivalent to “there exists a with s = {a}”, since every element of a group is a unit.

Русский

В группе для конечного множества s утверждение «существует a, такое что s = {a} и IsUnit(a)» эквивалентно «существует a, такое что s = {a}», поскольку каждый элемент группы является единичным.

LaTeX

$$$(\exists a, s = \{a\} \land IsUnit(a)) \iff (\exists a, s = \{a\})$$$

Lean4

@[simp]
theorem isUnit_iff_singleton_aux {α} [Group α] {s : Finset α} : (∃ a, s = { a } ∧ IsUnit a) ↔ ∃ a, s = { a } := by
  simp only [Group.isUnit, and_true]

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