Theorem IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin

Modification history

2025-10-09 13:58
Mathlib/NumberTheory/Cyclotomic/Basic.lean
feat(IsCyclotomicExtension): some results for the sub-algebra case (#29665) …
Added IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoinView on Github →