Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.mem_image_of_mem_map_of_surjective

Modification history

2018-12-20 08:13
ring_theory/ideal_operations.lean
feat(ring_theory/ideal_operations): correspondence under surjection (#534)
Added ideal.mem_image_of_mem_map_of_surjectiveView on Github →