Defs

📁 Source: Mathlib/RingTheory/Congruence/Defs.lean

Statistics

Metric	Count
Definitions RingCon, comap, hasNSMul, hasZSMul, instAddQuotient, instCoeTCQuotient, instCommRingQuotient, instCommSemiringQuotient, instDecidableEqQuotientOfDecidableCoeForallProp, instFunLikeForallProp, instInhabited, instInhabitedQuotient, instIntCastQuotient, instMulQuotient, instNatCastQuotient, instNegQuotient, instNonAssocRingQuotient, instNonAssocSemiringQuotient, instNonUnitalNonAssocRingQuotient, instNonUnitalNonAssocSemiringQuotient, instNonUnitalRingQuotient, instNonUnitalSemiringQuotient, instOneQuotient, instPowQuotientNat, instRingQuotient, instSemiringQuotient, instSubQuotient, instZeroQuotient, mk', toAddCon, toCon, toQuotient, ringConGen	33
Theorems add, add', coe_add, coe_inj, coe_intCast, coe_mk, coe_mk', coe_mul, coe_natCast, coe_neg, coe_nsmul, coe_one, coe_pow, coe_sub, coe_zero, coe_zsmul, comap_rel, eq, ext, ext', ext'', ext_iff, mk'_surjective, mul, neg, nsmul, quot_mk_eq_coe, refl, rel_eq_coe, rel_mk, sub, toCon_coe_eq_coe, toCon_inj, toCon_injective, trans, zsmul	36
Total	69

RingCon

Definitions

Name	Category	Theorems
comap 📖	CompOp	5 math math: comap_bot, ker_comp, comap_rel, comap_mono, comap_eq
hasNSMul 📖	CompOp	1 math math: coe_nsmul
hasZSMul 📖	CompOp	1 math math: coe_zsmul
instAddQuotient 📖	CompOp	16 math math: comapQuotientEquivRange_symm_mk, comapQuotientEquivOfSurj_symm_mk, comapQuotientEquivOfSurj_symm_mk', coe_add, comapQuotientEquivRangeS_symm_mk, comapQuotientEquivRange_mk, quotientQuotientEquivQuotient_coe_coe, quotientKerEquivOfRightInverse_apply, comapQuotientEquivRangeS_mk, coe_comapQuotientEquivRange_mk, coe_quotientKerEquivRangeS_mk, congr_mk, quotientQuotientEquivQuotient_mk_mk, quotientQuotientEquivQuotient_symm_mk, quotientKerEquivOfSurjective_mk, comapQuotientEquivOfSurj_mk
instCoeTCQuotient 📖	CompOp	—
instCommRingQuotient 📖	CompOp	—
instCommSemiringQuotient 📖	CompOp	—
instDecidableEqQuotientOfDecidableCoeForallProp 📖	CompOp	—
instFunLikeForallProp 📖	CompOp	40 math math: ker_apply, mapGen_apply_apply_of_surjective, coe_inj, rel_mk, sSup_def, TwoSidedIdeal.mem_mk, unop_iff, eq, TwoSidedIdeal.ker_ringCon, sup_def, inf_iff_and, ofMatrix_rel, op_iff, comap_rel, coe_inf, coe_ofMatrix_eq_relationMap, sSup_eq_ringConGen, ringConGen_of_ringCon, refl, ofMatrix_rel', coe_iInf, le_def, TwoSidedIdeal.rel_iff, coe_mk, factorₐ_apply, TwoSidedIdeal.coe_mk, matrix_apply_single, coe_sInf, ext_iff, coe_bot, quot_mk_eq_coe, TwoSidedIdeal.mem_iff, ringConGen_idem, coe_top, rel_eq_coe, matrix_apply, toCon_coe_eq_coe, map_apply, sup_eq_ringConGen, mapGen_eq_map_of_surjective
instInhabited 📖	CompOp	—
instInhabitedQuotient 📖	CompOp	—
instIntCastQuotient 📖	CompOp	—
instMulQuotient 📖	CompOp	19 math math: smulCommClass, comapQuotientEquivRange_symm_mk, isScalarTower_right, comapQuotientEquivOfSurj_symm_mk, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivRangeS_symm_mk, comapQuotientEquivRange_mk, quotientQuotientEquivQuotient_coe_coe, quotientKerEquivOfRightInverse_apply, comapQuotientEquivRangeS_mk, coe_mul, smulCommClass', coe_comapQuotientEquivRange_mk, coe_quotientKerEquivRangeS_mk, congr_mk, quotientQuotientEquivQuotient_mk_mk, quotientQuotientEquivQuotient_symm_mk, quotientKerEquivOfSurjective_mk, comapQuotientEquivOfSurj_mk
instNatCastQuotient 📖	CompOp	2 math math: coe_natCast, coe_intCast
instNegQuotient 📖	CompOp	1 math math: coe_neg
instNonAssocRingQuotient 📖	CompOp	—
instNonAssocSemiringQuotient 📖	CompOp	33 math math: Quotient.hom_ext_iff, lift_comp_mk', comapQuotientEquivRange_symm_mk, rangeS_kerLift, comapQuotientEquivRangeS_symm_mk, comapQuotientEquivRange_mk, mk'_surjective, lift_apply_mk', lift_surjective_iff, quotientQuotientEquivQuotient_coe_coe, lift_bijective_iff, quotientKerEquivOfRightInverse_apply, comapQuotientEquivRangeS_mk, coe_comapQuotientEquivRange_mk, quotientQuotientEquivQuotientₐ_mk_mk, quotientQuotientEquivQuotient_mk_mk, quotientQuotientEquivQuotientₐ_symm_mk, kerLift_injective, ker_mk'_eq, lift_surjective_of_surjective, kerLift_mk, lift_mk', rangeS_mk', coe_mk', rangeS_lift, quotientQuotientEquivQuotient_symm_mk, coe_liftₐ, TwoSidedIdeal.ker_ringCon_mk', quotientQuotientEquivQuotientₐ_coe_coe, map_apply, lift_injective_iff, comap_eq, lift_coe
instNonUnitalNonAssocRingQuotient 📖	CompOp	—
instNonUnitalNonAssocSemiringQuotient 📖	CompOp	—
instNonUnitalRingQuotient 📖	CompOp	—
instNonUnitalSemiringQuotient 📖	CompOp	—
instOneQuotient 📖	CompOp	1 math math: coe_one
instPowQuotientNat 📖	CompOp	1 math math: coe_pow
instRingQuotient 📖	CompOp	6 math math: comapQuotientEquivRange_symm_mk, comapQuotientEquivRange_mk, coe_comapQuotientEquivRange_mk, kerLift_range_eq, range_mk', range_lift
instSemiringQuotient 📖	CompOp	24 math math: quotientKerEquivRangeₐ_comp_mkₐ, coe_comapQuotientEquivRangeₐ_mk, mkₐ_comp_factorₐ_comp_mkₐ, kerLiftₐ_mk, factorₐ_mk, coe_algebraMap, congrₐ_mk, kerLiftₐ_injective, kerLiftₐ_range_eq, quotientQuotientEquivQuotientₐ_mk_mk, coe_comapQuotientEquivRangeₐ_symm_mk, mkₐ_apply, comapQuotientEquivRangeₐ_mk, factorₐ_apply, mkₐ_surjective, quotientQuotientEquivQuotientₐ_symm_mk, quotientKerEquivRangeₐ_mkₐ, liftₐ_range, range_mkₐ, liftₐ_mk, coe_liftₐ, quotientQuotientEquivQuotientₐ_coe_coe, liftₐ_coe_toRingHom, coe_quotientKerEquivRangeₐ_mkₐ
instSubQuotient 📖	CompOp	1 math math: coe_sub
instZeroQuotient 📖	CompOp	1 math math: coe_zero
mk' 📖	CompOp	17 math math: Quotient.hom_ext_iff, lift_comp_mk', comapQuotientEquivRange_symm_mk, comapQuotientEquivRangeS_symm_mk, comapQuotientEquivRange_mk, mk'_surjective, lift_apply_mk', comapQuotientEquivRangeS_mk, coe_comapQuotientEquivRange_mk, ker_mk'_eq, range_mk', lift_mk', rangeS_mk', coe_mk', TwoSidedIdeal.ker_ringCon_mk', map_apply, comap_eq
toAddCon 📖	CompOp	—
toCon 📖	CompOp	17 math math: toCon_eq_bot, toCon_injective, TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, comapQuotientEquivOfSurj_symm_mk', sInf_toSetoid, toCon_inj, factorₐ_mk, quotientQuotientEquivQuotientₐ_mk_mk, quotientQuotientEquivQuotient_mk_mk, quotientQuotientEquivQuotientₐ_symm_mk, TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r, toCon_eq_top, rel_eq_coe, quotientQuotientEquivQuotient_symm_mk, toCon_coe_eq_coe, toCon_bot, toCon_top
toQuotient 📖	CompOp	42 math math: coe_zsmul, comapQuotientEquivRange_symm_mk, comapQuotientEquivOfSurj_symm_mk, coe_neg, coe_comapQuotientEquivRangeₐ_mk, comapQuotientEquivOfSurj_symm_mk', coe_add, eq, comapQuotientEquivRangeS_symm_mk, coe_one, coe_zero, comapQuotientEquivRange_mk, kerLiftₐ_mk, coe_smul, coe_nsmul, quotientQuotientEquivQuotient_coe_coe, comapQuotientEquivRangeS_mk, coe_algebraMap, coe_mul, congrₐ_mk, coe_comapQuotientEquivRange_mk, coe_quotientKerEquivRangeS_mk, congr_mk, coe_comapQuotientEquivRangeₐ_symm_mk, mkₐ_apply, comapQuotientEquivRangeₐ_mk, factorₐ_apply, quot_mk_eq_coe, quotientKerEquivRangeₐ_mkₐ, kerLift_mk, coe_natCast, coe_mk', coe_intCast, liftₐ_mk, quotientKerEquivOfSurjective_mk, coe_sub, quotientQuotientEquivQuotientₐ_coe_coe, map_apply, coe_pow, coe_quotientKerEquivRangeₐ_mkₐ, comapQuotientEquivOfSurj_mk, lift_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	DFunLike.coe RingCon instFunLikeForallProp	—	—	add'
add' 📖	—	Con.toSetoid toCon	—	—	—
coe_add 📖	mathematical	—	toQuotient Quotient instAddQuotient	—	—
coe_inj 📖	mathematical	—	DFunLike.coe RingCon instFunLikeForallProp	—	—
coe_intCast 📖	mathematical	—	toQuotient AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toNatCast Quotient instNatCastQuotient	—	—
coe_mk 📖	mathematical	Con.toSetoid	DFunLike.coe RingCon instFunLikeForallProp Con Con.instFunLikeForallProp	—	—
coe_mk' 📖	mathematical	—	DFunLike.coe RingHom Quotient Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul instNonAssocSemiringQuotient RingHom.instFunLike mk' toQuotient	—	—
coe_mul 📖	mathematical	—	toQuotient Quotient instMulQuotient	—	—
coe_natCast 📖	mathematical	—	toQuotient AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toNatCast Quotient instNatCastQuotient	—	—
coe_neg 📖	mathematical	—	toQuotient AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Quotient instNegQuotient	—	—
coe_nsmul 📖	mathematical	—	toQuotient AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.toNatSMul Quotient hasNSMul	—	—
coe_one 📖	mathematical	—	toQuotient MulOne.toMul MulOneClass.toMulOne MulOne.toOne Quotient instOneQuotient	—	—
coe_pow 📖	mathematical	—	toQuotient MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Monoid.toNatPow Quotient instPowQuotientNat	—	—
coe_sub 📖	mathematical	—	toQuotient AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toSub Quotient instSubQuotient	—	—
coe_zero 📖	mathematical	—	toQuotient AddZero.toAdd AddZeroClass.toAddZero AddZero.toZero Quotient instZeroQuotient	—	—
coe_zsmul 📖	mathematical	—	toQuotient AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul Quotient hasZSMul	—	—
comap_rel 📖	mathematical	—	DFunLike.coe RingCon instFunLikeForallProp comap	—	—
eq 📖	mathematical	—	toQuotient DFunLike.coe RingCon instFunLikeForallProp	—	Quotient.eq''
ext 📖	—	DFunLike.coe RingCon instFunLikeForallProp	—	—	ext'
ext' 📖	—	DFunLike.coe RingCon instFunLikeForallProp	—	—	DFunLike.coe_injective
ext'' 📖	—	Con.toSetoid toCon	—	—	ext Setoid.ext_iff
ext_iff 📖	mathematical	—	DFunLike.coe RingCon instFunLikeForallProp	—	ext
mk'_surjective 📖	mathematical	—	Quotient Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul DFunLike.coe RingHom instNonAssocSemiringQuotient RingHom.instFunLike mk'	—	Quotient.mk''_surjective
mul 📖	—	DFunLike.coe RingCon instFunLikeForallProp	—	—	Con.mul'
neg 📖	mathematical	DFunLike.coe RingCon AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLikeForallProp	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	AddCon.neg
nsmul 📖	mathematical	DFunLike.coe RingCon AddSemigroup.toAdd AddMonoid.toAddSemigroup instFunLikeForallProp	AddMonoid.toNatSMul	—	AddCon.nsmul
quot_mk_eq_coe 📖	mathematical	—	DFunLike.coe RingCon instFunLikeForallProp toQuotient	—	—
refl 📖	mathematical	—	DFunLike.coe RingCon instFunLikeForallProp	—	Setoid.refl'
rel_eq_coe 📖	mathematical	—	Con.toSetoid toCon DFunLike.coe RingCon instFunLikeForallProp	—	—
rel_mk 📖	mathematical	Con.toSetoid	DFunLike.coe RingCon instFunLikeForallProp Con Con.instFunLikeForallProp	—	—
sub 📖	mathematical	DFunLike.coe RingCon AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLikeForallProp	SubNegMonoid.toSub	—	AddCon.sub
toCon_coe_eq_coe 📖	mathematical	—	DFunLike.coe Con Con.instFunLikeForallProp toCon RingCon instFunLikeForallProp	—	—
toCon_inj 📖	mathematical	—	toCon	—	toCon_injective
toCon_injective 📖	mathematical	—	RingCon Con toCon	—	add'
trans 📖	—	DFunLike.coe RingCon instFunLikeForallProp	—	—	Setoid.trans'
zsmul 📖	mathematical	DFunLike.coe RingCon AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLikeForallProp	SubNegMonoid.toZSMul	—	AddCon.zsmul

(root)

Definitions

Name	Category	Theorems
RingCon 📖	CompData	69 math math: TwoSidedIdeal.orderIsoRingCon_symm_apply, TwoSidedIdeal.ringCon_injective, RingCon.toCon_eq_bot, RingCon.ker_apply, TwoSidedIdeal.ringCon_le_iff, RingCon.coe_inj, RingCon.rel_mk, TwoSidedIdeal.orderIsoRingCon_apply, RingCon.sSup_def, RingCon.comap_bot, RingCon.matrix_strictMono_of_nonempty, RingCon.matrix_top, RingCon.toCon_injective, TwoSidedIdeal.iSup_ringCon, TwoSidedIdeal.mem_mk, TwoSidedIdeal.iInf_ringCon, RingCon.unop_iff, RingCon.eq, TwoSidedIdeal.ker_ringCon, RingCon.sup_def, RingCon.subsingleton_quotient, RingCon.inf_iff_and, RingCon.ofMatrix_rel, RingCon.ringConGen_eq, RingCon.op_iff, RingCon.comap_rel, RingCon.coe_inf, RingCon.sInf_toSetoid, RingCon.coe_ofMatrix_eq_relationMap, RingCon.sSup_eq_ringConGen, RingCon.instNontrivial, TwoSidedIdeal.sInf_ringCon, RingCon.ringConGen_of_ringCon, RingCon.opOrderIso_apply, RingCon.nontrivial_iff, RingCon.refl, RingCon.ofMatrix_rel', TwoSidedIdeal.sSup_ringCon, RingCon.coe_iInf, RingCon.le_def, TwoSidedIdeal.rel_iff, RingCon.coe_mk, RingCon.opOrderIso_symm_apply, RingCon.matrix_injective, TwoSidedIdeal.coe_mk, RingCon.matrix_bot, RingCon.matrix_apply_single, RingCon.coe_sInf, RingCon.ext_iff, RingCon.coe_bot, RingCon.quot_mk_eq_coe, TwoSidedIdeal.mem_iff, TwoSidedIdeal.top_ringCon, TwoSidedIdeal.sup_ringCon, RingCon.subsingleton_iff, RingCon.ringConGen_idem, RingCon.toCon_eq_top, TwoSidedIdeal.bot_ringCon, RingCon.coe_top, RingCon.rel_eq_coe, RingCon.instSubsingleton, RingCon.matrix_apply, RingCon.toCon_coe_eq_coe, TwoSidedIdeal.inf_ringCon, RingCon.sup_eq_ringConGen, RingCon.matrix_monotone, RingCon.ringConGen_mono, RingCon.toCon_bot, RingCon.toCon_top
ringConGen 📖	CompOp	9 math math: RingCon.sSup_def, RingCon.sup_def, RingCon.ringConGen_eq, RingCon.sSup_eq_ringConGen, RingCon.ringConGen_of_ringCon, RingCon.ringConGen_le, RingCon.ringConGen_idem, RingCon.sup_eq_ringConGen, RingCon.ringConGen_mono

---

← Back to Index