mul_notMem_of_exponent_two — Mathlib

English

If exponent G = 2, then for distinct x,y ≠ 1, xy ∉ {x,y,1}.

Русский

Если экспонента G = 2, то для различных x,y ≠ 1, xy ∉ {x,y,1}.

LaTeX

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

Lean4

@[to_additive]
theorem mul_notMem_of_exponent_two (h : Monoid.exponent G = 2) {x y : G} (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) :
    x * y ∉ ({ x, y, 1 } : Set G) :=
  mul_notMem_of_orderOf_eq_two (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one x) hx)
    (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one y) hy) hxy

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