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.

Estimated changes