Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-20 08:13 bc21f62e

View on Github →

feat(ring_theory/ideal_operations): correspondence under surjection (#534)

Estimated changes

Modified ring_theory/ideal_operations.lean

added theorem ideal.comap_map_of_surjective

added def ideal.le_order_embedding_of_surjective

added def ideal.lt_order_embedding_of_surjective

added theorem ideal.map_comap_of_surjective

added theorem ideal.mem_image_of_mem_map_of_surjective

added def ideal.order_iso_of_surjective