Commit 2021-09-07 11:06 d366eb3d

View on Github →

feat(ring_theory/ideal/operations): add some theorems about taking the quotient of a ring by a sum of ideals (#8668) The aim of this section is to prove that if I, J are ideals of the ring R, then the quotients R/(I+J) and (R/I)/J'are isomorphic, where J' is the image of J in R/I.

Estimated changes

Modified src/ring_theory/ideal/basic.lean

added def ideal.quotient.factor

added theorem ideal.quotient.factor_comp_mk

added theorem ideal.quotient.factor_mk

Modified src/ring_theory/ideal/operations.lean

added theorem double_quot.ker_quot_left_to_quot_sup

added theorem double_quot.ker_quot_quot_mk

added def double_quot.lift_sup_quot_quot_mk

added def double_quot.quot_left_to_quot_sup

added def double_quot.quot_quot_equiv_quot_sup

added def double_quot.quot_quot_mk

added def double_quot.quot_quot_to_quot_sup

added theorem ideal.ker_quotient_lift

added theorem ideal.map_eq_iff_sup_ker_eq_of_surjective

added theorem ideal.map_mk_eq_bot_of_le