eq_finset_univ — Mathlib

English

In a Klein four group, if x,y ≠ 1 and x ≠ y, then the set {xy, x, y, 1} equals the whole group.

Русский

В группе Klein Four, если x ≠ 1, y ≠ 1 и x ≠ y, то множество {xy, x, y, 1} равно всей группе.

LaTeX

$${xy, x, y, 1} = Finset.univ$$

Lean4

@[to_additive]
theorem eq_finset_univ [Fintype G] [DecidableEq G] {x y : G} (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) :
    {x * y, x, y, (1 : G)} = Finset.univ := by
  apply Finset.eq_univ_of_card
  rw [card_four']
  repeat rw [card_insert_of_notMem]
  on_goal 4 => simpa using mul_notMem_of_exponent_two (by simp) hx hy hxy
  all_goals simp_all

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