nthRoots_one_eq_biUnion_primitiveRoots

English

The set nthRootsFinset n 1 is equal to the union, over i dividing n, of primitiveRoots i R.

Русский

Множество nthRootsFinset n 1 равно объединению по i|n множеств primitiveRoots i R.

LaTeX

$$$\operatorname{nthRootsFinset}(n,1) = \bigcup_{i \mid n} \operatorname{primitiveRoots}(i,R)$$$

Lean4

/-- `nthRoots n` as a `Finset` is equal to the union of `primitiveRoots i R` for `i ∣ n`. -/
theorem nthRoots_one_eq_biUnion_primitiveRoots [DecidableEq R] {n : ℕ} :
    nthRootsFinset n (1 : R) = (Nat.divisors n).biUnion fun i ↦ primitiveRoots i R :=
  by
  by_cases hn : n = 0
  · simp only [hn, nthRootsFinset_zero, Nat.divisors_zero, biUnion_empty]
  have : NeZero n := ⟨hn⟩
  exact nthRoots_one_eq_biUnion_primitiveRoots'

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