Theorems · Theorem · number theory
IsCyclotomicExtension.Rat.associated_sub_one_of_isPrimitiveRoot
∀ (p : ℕ) {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [inst_1 : NeZero p] {η : K}
(hη : IsPrimitiveRoot η p), Associated (hζ.toInteger - 1) (hη.toInteger - 1)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- NumberField.RingOfIntegersstatement and proof · cited by 413
- IsPrimitiveRootstatement and proof · cited by 356
- Associatedstatement and proof · cited by 296
- IsPrimitiveRoot.toIntegerstatement and proof · cited by 72
- IsPrimitiveRoot.toInteger_isPrimitiveRootproof · cited by 15
- NumberField.RingOfIntegers.extproof · cited by 10
- IsPrimitiveRoot.isPrimitiveRoot_iffproof · cited by 3
- IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprimeproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.Rat.associated_zeta_sub_one_pow_primeproof · cited by 1