eq_mul_of_ne_all — Mathlib

English

In a Klein four group, if x,y,z are non-identity and pairwise distinct, then z = x y.

Русский

В группе Klein Four, если x,y,z не единицы и попарно различны, то z = x y.

LaTeX

$$x ≠ 1 \land y ≠ 1 \land x ≠ y \land z ≠ 1 \land z ≠ x \land z ≠ y \Rightarrow z = x y$$

Lean4

@[to_additive]
theorem eq_mul_of_ne_all {x y z : G} (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) (hz : z ≠ 1) (hzx : z ≠ x) (hzy : z ≠ y) :
    z = x * y := by
  classical
  let _ := Fintype.ofFinite G
  apply eq_of_mem_insert_of_notMem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _
  simpa only [mem_singleton, mem_insert, not_or] using ⟨hzx, hzy, hz⟩

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