Commit 2024-05-28 19:50 1d666fda
View on Github →chore: Do not import LinearOrderedField in Algebra.Module.Defs (#13274)
The single abel call in Algebra.Module.Defs meant that the definition of Module imported norm_num, which imports LinearOrderedField to represent numerals. Dumb down the proof to a rw call.
Combined with #13305, Algebra.Module.Defs goes from 661 dependencies to 523.