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) …
Added X_pow_sub_C_eq_prod'View on Github →