Commit 2021-10-18 17:55 b112d4dd

View on Github →

refactor(ring_theory/ideal/operations): generalize various definitions to remove negation and commutativity (#9737) Mostly this just weakens assumptions in variables lines, but occasionally this moves lemmas to a more appropriate section too.

Estimated changes

Modified src/ring_theory/ideal/operations.lean

modified theorem ideal.comap_is_maximal_of_surjective

modified theorem ideal.comap_le_iff_le_map

modified theorem ideal.comap_map_of_surjective

modified theorem ideal.map.is_maximal

modified theorem ideal.map_eq_top_or_is_maximal_of_surjective

modified def ideal.rel_iso_of_surjective

modified theorem ideal.subset_union

modified theorem ideal.subset_union_prime'

modified theorem ideal.subset_union_prime

Modified src/ring_theory/jacobson.lean