Commit 2023-03-09 08:47 43fb515a

View on Github →

feat: port RingTheory.Ideal.Quotient (#2412)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Quotient.lean

added theorem Ideal.Quotient.eq_zero_iff_mem

added theorem Ideal.Quotient.exists_inv

added def Ideal.Quotient.factor

added theorem Ideal.Quotient.factor_comp_mk

added theorem Ideal.Quotient.factor_mk

added theorem Ideal.Quotient.isDomain_iff_prime

added def Ideal.Quotient.lift

added theorem Ideal.Quotient.lift_mk

added theorem Ideal.Quotient.lift_surjective_of_surjective

added theorem Ideal.Quotient.maximal_ideal_iff_isField_quotient

added theorem Ideal.Quotient.maximal_of_isField

added def Ideal.Quotient.mk

added theorem Ideal.Quotient.mk_eq_mk

added theorem Ideal.Quotient.mk_eq_mk_iff_sub_mem

added theorem Ideal.Quotient.mk_surjective

added theorem Ideal.Quotient.quotient_ring_saturate

added theorem Ideal.Quotient.ringHom_ext

added theorem Ideal.Quotient.subsingleton_iff

added theorem Ideal.Quotient.zero_eq_one_iff

added theorem Ideal.Quotient.zero_ne_one_iff

added theorem Ideal.exists_sub_mem

added theorem Ideal.exists_sub_one_mem_and_mem

added theorem Ideal.fst_comp_quotientInfEquivQuotientProd

added theorem Ideal.map_pi

added def Ideal.quotEquivOfEq

added theorem Ideal.quotEquivOfEq_mk

added theorem Ideal.quotEquivOfEq_symm

added theorem Ideal.quotientInfEquivQuotientProd_fst

added theorem Ideal.quotientInfEquivQuotientProd_snd

added def Ideal.quotientInfToPiQuotient

added theorem Ideal.quotientInfToPiQuotient_bijective

added theorem Ideal.snd_comp_quotientInfEquivQuotientProd