Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.quotient.mk_sum

Modification history

2020-07-21 01:05
src/ring_theory/ideals.lean
refactor(ring_theory): remove unbundled leftovers in `ideal.quotient` (#3467) …
Deleted ideal.quotient.mk_sumView on Github →
2020-03-13 09:00
src/ring_theory/ideals.lean
refactor(*): migrate some files to bundled ring homs (#2133) …
Added ideal.quotient.mk_sumView on Github →