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.