Commit 2023-05-24 22:02 2cbf1894

View on Github →

feat: Double quotient of an algebra (#3750) Match https://github.com/leanprover-community/mathlib/pull/18452 ring_theory.ideal.quotient_operations@d3acee0d776b15ffb8318f327325ff343cc8bdcc..b88d81c84530450a8989e918608e5960f015e6c8

Estimated changes

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

added theorem DoubleQuot.coe_liftSupQuotQuotMkₐ

added theorem DoubleQuot.coe_quotLeftToQuotSupₐ

added theorem DoubleQuot.coe_quotQuotEquivCommₐ

added theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ

added theorem DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm

added theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ

added theorem DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm

added theorem DoubleQuot.coe_quotQuotMkₐ

added theorem DoubleQuot.coe_quotQuotToQuotSupₐ

added def DoubleQuot.liftSupQuotQuotMkₐ

added theorem DoubleQuot.liftSupQuotQuotMkₐ_toRingHom

added def DoubleQuot.quotLeftToQuotSupₐ

added theorem DoubleQuot.quotLeftToQuotSupₐ_toRingHom

added theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ

added theorem DoubleQuot.quotQuotEquivComm_symmₐ

added def DoubleQuot.quotQuotEquivCommₐ

added theorem DoubleQuot.quotQuotEquivCommₐ_toRingEquiv

added def DoubleQuot.quotQuotEquivQuotOfLE

added theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk

added theorem DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ

added theorem DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk

added theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk

added theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ

added theorem DoubleQuot.quotQuotEquivQuotOfLE_symm_mk

added def DoubleQuot.quotQuotEquivQuotOfLEₐ

added theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv

added theorem DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv

deleted def DoubleQuot.quotQuotEquivQuotOfLe

deleted theorem DoubleQuot.quotQuotEquivQuotOfLe_comp_quotQuotMk

deleted theorem DoubleQuot.quotQuotEquivQuotOfLe_quotQuotMk

deleted theorem DoubleQuot.quotQuotEquivQuotOfLe_symm_comp_mk

deleted theorem DoubleQuot.quotQuotEquivQuotOfLe_symm_mk

added def DoubleQuot.quotQuotEquivQuotSupₐ

added theorem DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv

added theorem DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv

added def DoubleQuot.quotQuotMkₐ

added theorem DoubleQuot.quotQuotMkₐ_toRingHom

added def DoubleQuot.quotQuotToQuotSupₐ

added theorem DoubleQuot.quotQuotToQuotSupₐ_toRingHom