disjoint — Mathlib

English

The sets primitiveRoots k R and primitiveRoots l R are disjoint when k ≠ l.

Русский

Множества primitiveRoots k R и primitiveRoots l R попарно не пересекаются при k ≠ l.

LaTeX

$$Disjoint(primitiveRoots(k,R), primitiveRoots(l,R)) при k ≠ l$$

Lean4

/-- The sets `primitiveRoots k R` are pairwise disjoint. -/
theorem disjoint {k l : ℕ} (h : k ≠ l) : Disjoint (primitiveRoots k R) (primitiveRoots l R) :=
  Finset.disjoint_left.2 fun _ hk hl ↦
    h <| (isPrimitiveRoot_of_mem_primitiveRoots hk).unique <| isPrimitiveRoot_of_mem_primitiveRoots hl

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