Theorems · Theorem · number theory
IsPrimitiveRoot.injOn_pow_mul
∀ {M₀ : Type u_7} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] {n : ℕ} {ζ : M₀},
IsPrimitiveRoot ζ n → ∀ {α : M₀}, α ≠ 0 → Set.InjOn (fun x => ζ ^ x * α) ↑(Finset.range n)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Finset.rangestatement and proof · cited by 1,341
- CommMonoidWithZerostatement and proof · cited by 913
- Set.InjOnstatement · cited by 543
- IsPrimitiveRootstatement and proof · cited by 356
- IsCancelMulZerostatement and proof · cited by 177
- IsPrimitiveRoot.injOn_powproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.nthRoots_eqproof · cited by 3
- Polynomial.separable_X_pow_sub_C_of_irreducibleproof · cited by 1
- IsPrimitiveRoot.nthRoots_nodupproof · cited by 1