Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-23 11:01 2b79f1da

View on Github →

feat(ring_theory/ideal_operations): lemmas about ideals and galois connections (#2767) depends on #2766

Estimated changes

added theorem monotone.le_map_Sup
added theorem monotone.map_Inf_le
added theorem ideal.comap_Inf
added theorem ideal.comap_comap
added theorem ideal.comap_id
added theorem ideal.comap_infi
added theorem ideal.comap_map_comap
modified theorem ideal.comap_top
added theorem ideal.gc_map_comap
added theorem ideal.le_comap_map
added theorem ideal.map_Sup
modified theorem ideal.map_bot
added theorem ideal.map_comap_le
added theorem ideal.map_comap_map
added theorem ideal.map_id
added theorem ideal.map_map
modified theorem ideal.map_sup
added theorem ideal.map_supr
added theorem ideal.mul_le_left
added theorem ideal.mul_le_right
modified theorem submodule.annihilator_supr
modified theorem submodule.infi_colon_supr