Theorem IsCyclotomicExtension.Rat.Three.coe_eta

Modification history

2024-06-25 09:57

Mathlib/NumberTheory/Cyclotomic/Three.lean

feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798) …

Added IsCyclotomicExtension.Rat.Three.coe_eta View on Github →