Commit 2023-04-21 08:03 4bef854a

View on Github →

feat: port Algebra.RingQuot (#3383)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/RingQuot.lean

added theorem RingCon.coe_algebraMap

added theorem RingQuot.Rel.add_right

added theorem RingQuot.Rel.neg

added theorem RingQuot.Rel.smul

added theorem RingQuot.Rel.star

added theorem RingQuot.Rel.sub_left

added theorem RingQuot.Rel.sub_right

added inductive RingQuot.Rel

added theorem RingQuot.add_quot

added theorem RingQuot.eq_liftAlgHom_comp_mkAlgHom

added theorem RingQuot.eq_lift_comp_mkRingHom

added theorem RingQuot.eqvGen_rel_eq

added def RingQuot.idealQuotientToRingQuot

added theorem RingQuot.idealQuotientToRingQuot_apply

added theorem RingQuot.liftAlgHom_mkAlgHom_apply

added theorem RingQuot.liftAlgHom_unique

added theorem RingQuot.lift_mkRingHom_apply

added theorem RingQuot.lift_unique

added theorem RingQuot.mkAlgHom_coe

added theorem RingQuot.mkAlgHom_rel

added theorem RingQuot.mkAlgHom_surjective

added theorem RingQuot.mkRingHom_rel

added theorem RingQuot.mkRingHom_surjective

added theorem RingQuot.mul_quot

added theorem RingQuot.neg_quot

added theorem RingQuot.one_quot

added theorem RingQuot.pow_quot

added def RingQuot.ringCon

added def RingQuot.ringQuotEquivIdealQuotient

added def RingQuot.ringQuotToIdealQuotient

added theorem RingQuot.ringQuotToIdealQuotient_apply

added theorem RingQuot.ringQuot_ext'

added theorem RingQuot.ringQuot_ext

added theorem RingQuot.smul_quot

added theorem RingQuot.star'_quot

added def RingQuot.starRing

added theorem RingQuot.sub_quot

added theorem RingQuot.zero_quot

added structure RingQuot

Modified Mathlib/RingTheory/Ideal/Quotient.lean