Theorems · Theorem · number theory
IsPrimitiveRoot.coe_submonoidClass_iff
∀ {k : ℕ} {M : Type u_7} {B : Type u_8} [inst : CommMonoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M]
{N : B} {ζ : ↥N}, IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k- Cited by
- 11 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommMonoidstatement and proof · cited by 2,264
- SetLikestatement and proof · cited by 1,084
- IsPrimitiveRootstatement · cited by 356
- SubmonoidClassstatement and proof · cited by 60
Cited by11
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
- IsPrimitiveRoot.adjoin_isCyclotomicExtensionproof · cited by 3
- IsCyclotomicExtension.Rat.adjoin_singleton_eq_topproof · cited by 3
- IsPrimitiveRoot.idealQuotient_mkproof · cited by 1
- IsCyclotomicExtension.Rat.discrproof · cited by 1
- IsCyclotomicExtension.eqproof · cited by 1
- card_rootsOfUnity_eq_iff_exists_isPrimitiveRootproof · cited by 1
- IsPrimitiveRoot.prime_dvd_of_dvd_norm_sub_oneproof · cited by 1
- IsCyclotomicExtension.union_leftproof · cited by 1
- IsCyclotomicExtension.Rat.torsionOrder_eqproof · cited by 0
- MulEquiv.hasEnoughRootsOfUnityproof · cited by 0