mathlib
e4e07eab - feat(ring_theory): `map f (span s) = span (f '' s)` (#9068)

Commit

4 years ago

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.

Author

Vierkantor

Parents