Mathlib v3 is deprecated. Go to Mathlib v4

Def cyclotomic_field.algebra_base

Modification history

2023-05-22 12:50
src/number_theory/cyclotomic/basic.lean
feat(field_theory/splitting_field): fix the diamond (#18857) …
Deleted cyclotomic_field.algebra_baseView on Github →
2022-01-12 17:52
src/number_theory/cyclotomic/basic.lean
feat(number_theory/cyclotomic/basic): add cyclotomic_field and cyclotomic_ring (#11383) …
Added cyclotomic_field.algebra_baseView on Github →