Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 23:02 cc7627a6

View on Github →

feat(analysis/normed_space/basic): define normed_group structure induced by injective group homomorphism (#8443)

Estimated changes