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 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ₐ