Commit 2025-02-04 15:13 1cca6b8e

View on Github →

refactor: introduce Ideal.IsTwoSided class for quotients of noncommutative rings (#17930)

Estimated changes

modified theorem Module.IsTorsionBy.mk_smul
modified theorem Module.Quotient.mk_smul_mk
modified def PadicInt.residueField
modified theorem Ideal.annihilator_quotient
modified theorem Submodule.colon_top
modified theorem Ideal.mul_mem_right
modified theorem Ideal.mul_sub_mul_mem
modified theorem Ideal.mul_le_right
modified theorem Ideal.mul_right_self_sup
modified theorem Ideal.sup_mul_right_self
modified theorem Ideal.Quotient.exists_inv
modified theorem Ideal.map_pi
modified def Ideal.Quotient.factor
modified theorem Ideal.Quotient.factor_mk
modified def Ideal.Quotient.lift
modified theorem Ideal.Quotient.lift_mk
modified def Ideal.Quotient.mk
modified def Ideal.quotEquivOfEq
modified theorem Ideal.quotEquivOfEq_mk
modified theorem Ideal.quotEquivOfEq_symm
modified theorem Ideal.Quotient.algHom_ext
modified theorem Ideal.Quotient.alg_map_eq
modified theorem Ideal.Quotient.liftₐ_comp
modified def Ideal.Quotient.mkₐ
modified theorem Ideal.Quotient.mkₐ_eq_mk
modified theorem Ideal.Quotient.mkₐ_ker
modified theorem Ideal.comap_map_mk
modified theorem Ideal.injective_lift_iff
modified theorem Ideal.ker_Pi_Quotient_mk
modified theorem Ideal.ker_quotientMap_mk
modified theorem Ideal.ker_quotient_lift
modified theorem Ideal.map_mk_eq_bot_of_le
modified theorem Ideal.map_quotient_self
modified theorem Ideal.mem_quotient_iff_mem
modified theorem Ideal.mk_ker
modified def Ideal.quotientEquiv
modified theorem Ideal.quotientEquiv_mk
modified theorem Ideal.quotientEquiv_symm_mk
modified def Ideal.quotientMap
modified theorem Ideal.quotientMap_comp_mk
modified theorem Ideal.quotientMap_injective
modified theorem Ideal.quotientMap_mk
modified def Ideal.quotientMapₐ
modified theorem Ideal.quotient_map_mkₐ