Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 15:48 e8427b03

View on Github →

feat(ring_theory/ideal/operation): add some extra definitions in the double_quot section (#9649)

Estimated changes

Modified src/ring_theory/ideal/operations.lean

added def double_quot.quot_quot_equiv_comm

added theorem double_quot.quot_quot_equiv_comm_comp_quot_quot_mk

added theorem double_quot.quot_quot_equiv_comm_quot_quot_mk

added theorem double_quot.quot_quot_equiv_comm_symm

added theorem double_quot.quot_quot_equiv_quot_sup_quot_quot_mk

added theorem double_quot.quot_quot_equiv_quot_sup_symm_quot_quot_mk