Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-08 12:15 e4e07eab

View on Github →

feat(ring_theory): map f (span s) = span (f '' s) (#9068) We already had this for submodules and linear maps, here it is for ideals and ring homs.

Estimated changes