Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-05 11:51 97cd01b0

View on Github →

refactor(linear_algebra/quotient_module): avoid using type class inference for setoids (#310) Continuation of #212 . Avoid using type class inference for quotient modules, and introduce a version of quotient.mk specifically for quotient modules, whose output type is quotient β s rather than quotient (quotient_rel s), which should help type class inference.

Estimated changes