Theorem IsCyclotomicExtension.empty

Modification history

2025-10-09 13:58
Mathlib/NumberTheory/Cyclotomic/Basic.lean
feat(IsCyclotomicExtension): some results for the sub-algebra case (#29665) …
Deleted IsCyclotomicExtension.emptyView on Github →
2023-06-22 09:14
Mathlib/NumberTheory/Cyclotomic/Basic.lean
feat: port NumberTheory.Cyclotomic.Basic (#5335)
Added IsCyclotomicExtension.emptyView on Github →