Theorem submodule.map_infi_comap_of_surjective
Modification history
2022-01-18 17:08
src/linear_algebra/basic.lean
feat(linear_algebra,algebra,group_theory): miscellaneous lemmas linking some additive monoid and module operations (#11525) …
Modified submodule.map_infi_comap_of_surjectiveView on Github →