Commit 2022-03-16 15:39 693a3ac9

View on Github →

feat(number_theory/cyclotomic/basic): add is_primitive_root.adjoin (#12716) We add is_cyclotomic_extension.is_primitive_root.adjoin. From flt-regular

Estimated changes

Modified src/number_theory/cyclotomic/basic.lean

added theorem is_primitive_root.adjoin_is_cyclotomic_extension

Modified src/number_theory/cyclotomic/primitive_roots.lean