Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.map_comap_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.map_comap_of_surjective View on Github →