Theorem IsCyclotomicExtension.Rat.Three.eta_sq

Modification history

2025-07-11 09:29
Mathlib/NumberTheory/Cyclotomic/Three.lean
chore: a batch of whitespace fixes (#26964) …
Modified IsCyclotomicExtension.Rat.Three.eta_sqView on Github →
2024-07-11 10:12
Mathlib/NumberTheory/Cyclotomic/Three.lean
feat(Mathlib.NumberTheory.FLT.Three): add various results (#14227) …
Added IsCyclotomicExtension.Rat.Three.eta_sqView on Github →