Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-14 06:55 4b262b84

View on Github →

refactor(topology/algebra/module/basic): don't import determinant (#17517) More files on the longest import chain in mathlib.

Estimated changes