Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 10:15 9dd8ec1e

View on Github →

feat(analysis/normed/group/hom): add a module instance (#12465)

Estimated changes