mathlib

16cf14f1 - feat(number_theory/cyclotomic/rat): add integral_power_basis (#15570)

feat(number_theory/cyclotomic/rat): add integral_power_basis (#15570) We add `integral_power_basis` and some variants, defining integral power basis of `𝓞 K`. From flt-regular