Theorem X_pow_sub_C_eq_prod

Modification history

2024-05-28 11:56
Mathlib/FieldTheory/KummerExtension.lean
feat(RingTheory/RootsOfUnity): product representation of the order of a primitive root of unity (#13290) …
Modified X_pow_sub_C_eq_prodView on Github →
2023-12-30 19:16
Mathlib/FieldTheory/KummerExtension.lean
feat: Kummer extensions are cyclic. (#9119)
Added X_pow_sub_C_eq_prodView on Github →