basic): add missing lemmas (#11451)

Commit

4 years ago

feat(number_theory/cyclotomic/basic): add missing lemmas (#11451) We add some missing lemmas about cyclotomic extensions. From flt-regular.

Author

riccardobrasca

Parents