mul_notMem_of_orderOf_eq_two — Mathlib

English

If x and y have order 2 and x ≠ y, then x y is not in {x,y,1}.

Русский

Если x и y имеют порядок 2 и x ≠ y, то x y не принадлежит {x, y, 1}.

LaTeX

$$$\forall x,y,\ orderOf(x)=2 \land orderOf(y)=2 \land x\neq y \Rightarrow xy \notin \{x,y,1\}$$$

Lean4

@[to_additive]
theorem mul_notMem_of_orderOf_eq_two {x y : G} (hx : orderOf x = 2) (hy : orderOf y = 2) (hxy : x ≠ y) :
    x * y ∉ ({ x, y, 1 } : Set G) :=
  by
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, mul_eq_left, mul_eq_right, mul_eq_one_iff_eq_inv,
    inv_eq_self_of_orderOf_eq_two hy, not_or]
  aesop

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