Commit 2024-01-31 20:39 a113026b
View on Github →feat: add Submodule.image_span_subset(_span) and golf (#10017)
Since Submodule.map requires surjectivity of the RingHom, the new lemmas have to be stated this way. (The RingHom is frobenius in my intended application, which is not necessarily surjective.)