Commit 2023-04-05 08:46 1bf712af

View on Github →

feat: port RingTheory.Ideal.QuotientOperations (#2757) "timeouts at whnf"s that I do not know what to do with.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/QuotientOperations.lean

added theorem DoubleQuot.ker_quotLeftToQuotSup

added theorem DoubleQuot.ker_quotQuotMk

added def DoubleQuot.liftSupQuotQuotMk

added def DoubleQuot.quotLeftToQuotSup

added def DoubleQuot.quotQuotEquivComm

added theorem DoubleQuot.quotQuotEquivComm_algebraMap

added theorem DoubleQuot.quotQuotEquivComm_comp_quotQuotMk

added theorem DoubleQuot.quotQuotEquivComm_mk_mk

added theorem DoubleQuot.quotQuotEquivComm_quotQuotMk

added theorem DoubleQuot.quotQuotEquivComm_symm

added def DoubleQuot.quotQuotEquivQuotOfLe

added theorem DoubleQuot.quotQuotEquivQuotOfLe_comp_quotQuotMk

added theorem DoubleQuot.quotQuotEquivQuotOfLe_quotQuotMk

added theorem DoubleQuot.quotQuotEquivQuotOfLe_symm_comp_mk

added theorem DoubleQuot.quotQuotEquivQuotOfLe_symm_mk

added def DoubleQuot.quotQuotEquivQuotSup

added theorem DoubleQuot.quotQuotEquivQuotSup_quotQuotMk

added theorem DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap

added theorem DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk

added def DoubleQuot.quotQuotMk

added def DoubleQuot.quotQuotToQuotSup

added theorem Ideal.KerLift.map_smul

added theorem Ideal.Quotient.algHom_ext

added theorem Ideal.Quotient.alg_map_eq

added theorem Ideal.Quotient.algebraMap_eq

added def Ideal.Quotient.liftₐ

added theorem Ideal.Quotient.liftₐ_apply

added theorem Ideal.Quotient.liftₐ_comp

added theorem Ideal.Quotient.mk_algebraMap

added theorem Ideal.Quotient.mk_comp_algebraMap

added def Ideal.Quotient.mkₐ

added theorem Ideal.Quotient.mkₐ_eq_mk

added theorem Ideal.Quotient.mkₐ_ker

added theorem Ideal.Quotient.mkₐ_surjective

added theorem Ideal.Quotient.mkₐ_toRingHom

added theorem Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply

added theorem Ideal.algebraMap_quotient_injective

added theorem Ideal.bot_quotient_isMaximal_iff

added theorem Ideal.comap_map_mk

added theorem Ideal.comp_quotientMap_eq_of_comp_eq

added def Ideal.kerLiftAlg

added theorem Ideal.kerLiftAlg_injective

added theorem Ideal.kerLiftAlg_mk

added theorem Ideal.kerLiftAlg_toRingHom

added theorem Ideal.ker_quotient_lift

added theorem Ideal.map_mk_eq_bot_of_le

added theorem Ideal.map_quotient_self

added theorem Ideal.mem_quotient_iff_mem

added theorem Ideal.mem_quotient_iff_mem_sup

added theorem Ideal.mk_ker

added def Ideal.quotientEquiv

added def Ideal.quotientEquivAlg

added def Ideal.quotientEquivAlgOfEq

added theorem Ideal.quotientEquivAlgOfEq_mk

added theorem Ideal.quotientEquivAlgOfEq_symm

added theorem Ideal.quotientEquiv_mk

added theorem Ideal.quotientEquiv_symm_mk

added theorem Ideal.quotientKerAlgEquivOfRightInverse.apply

added def Ideal.quotientKerAlgEquivOfRightInverse

added def Ideal.quotientMap

added theorem Ideal.quotientMap_algebraMap

added theorem Ideal.quotientMap_comp_mk

added theorem Ideal.quotientMap_injective'

added theorem Ideal.quotientMap_injective

added theorem Ideal.quotientMap_mk

added theorem Ideal.quotientMap_surjective

added def Ideal.quotientMapₐ

added theorem Ideal.quotient_map_comp_mkₐ

added theorem Ideal.quotient_map_mkₐ

added def RingHom.kerLift

added theorem RingHom.kerLift_injective

added theorem RingHom.kerLift_mk

added theorem RingHom.lift_injective_of_ker_le_ideal

added theorem RingHom.quotientKerEquivOfRightInverse.Symm.apply

added theorem RingHom.quotientKerEquivOfRightInverse.apply

added def RingHom.quotientKerEquivOfRightInverse