Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-26 09:29 40e97d37

View on Github →

feat(topology/algebra/module): ker, range, cod_restrict, subtype_val, coprod (#2525) Also move smul_right to general_ring and define some maps/equivalences useful for the inverse/implicit function theorem.

Estimated changes