Defs

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

Statistics

Metric	Count
Definitions AddCon, inhabited, nsmul, zsmul, addCommGroup, addCommMagma, addCommMonoid, addCommSemigroup, addGroup, addMonoid, addSemigroup, addZeroClass, comap, gi, hasAdd, hasNeg, hasSub, hrecOn₂, instCoeTCQuotient, instCompleteLattice, instDecidableEqQuotientOfDecidableCoeForallProp, instFunLikeForallProp, instInfSet, instInhabited, instLE, instMembershipProd, instPartialOrder, liftOn, liftOnAddUnits, liftOn₂, toQuotient, toSetoid, zero, Con, inhabited, comap, commGroup, commMagma, commMonoid, commSemigroup, gi, group, hasDiv, hasInv, hasMul, hrecOn₂, instCoeTCQuotient, instCompleteLattice, instDecidableEqQuotientOfDecidableCoeForallProp, instFunLikeForallProp, instInfSet, instInhabited, instLE, instMembershipProd, instPartialOrder, instPowQuotientNat, liftOn, liftOnUnits, liftOn₂, monoid, mulOneClass, one, semigroup, toQuotient, toSetoid, zpowinst, addConGen, conGen	68
Theorems add, add', addConGen_eq, addConGen_idem, addConGen_le, addConGen_mono, addConGen_of_addCon, coe_add, coe_iInf, coe_inf, coe_inj, coe_sInf, coe_zero, comap_rel, eq, ext, ext', ext_iff, hrec_on₂_coe, induction_on, induction_on_addUnits, induction_on₂, inf_iff_and, le_def, liftOnAddUnits_mk, liftOn_coe, map_of_add_left_rel_zero, neg, nsmul, quot_mk_eq_coe, refl, rel_eq_coe, rel_mk, sInf_toSetoid, sSup_def, sSup_eq_addConGen, sub, sup_def, sup_eq_addConGen, toSetoid_bot, toSetoid_eq_bot, toSetoid_eq_top, toSetoid_inj, toSetoid_injective, toSetoid_top, trans, zsmul, coe_iInf, coe_inf, coe_inj, coe_mul, coe_one, coe_sInf, comap_rel, conGen_eq, conGen_idem, conGen_le, conGen_mono, conGen_of_con, div, eq, ext, ext', ext_iff, hrec_on₂_coe, induction_on, induction_on_units, induction_on₂, inf_iff_and, inv, le_def, liftOnUnits_mk, liftOn_coe, map_of_mul_left_rel_one, mul, mul', pow, quot_mk_eq_coe, refl, rel_eq_coe, rel_mk, sInf_toSetoid, sSup_def, sSup_eq_conGen, sup_def, sup_eq_conGen, toSetoid_bot, toSetoid_eq_bot, toSetoid_eq_top, toSetoid_inj, toSetoid_injective, toSetoid_top, trans, zpow	94
Total	162

AddCon

Definitions

Name	Category	Theorems
addCommGroup 📖	CompOp	—
addCommMagma 📖	CompOp	—
addCommMonoid 📖	CompOp	—
addCommSemigroup 📖	CompOp	—
addGroup 📖	CompOp	—
addMonoid 📖	CompOp	—
addSemigroup 📖	CompOp	—
addZeroClass 📖	CompOp	18 math math: mk'_surjective, hom_ext_iff, lift_comp_mk', mrange_mk', comap_eq, coe_mk', kerLift_range_eq, kerLift_mk, mk'_ker, lift_mk', lift_range, kerLift_injective, lift_surjective_of_surjective, map_apply, lift_apply_mk', quotientKerEquivOfRightInverse_apply, lift_coe, coe_zero
comap 📖	CompOp	8 math math: comap_conGen_equiv, comapQuotientEquivOfSurj_symm_mk, comap_eq, comap_rel, comap_conGen_of_bijective, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, le_comap_conGen
gi 📖	CompOp	—
hasAdd 📖	CompOp	9 math math: ker_mkAddHom_eq, comapQuotientEquivOfSurj_symm_mk, coe_add, mkAddHom_apply, quotientKerEquivOfRightInverse_apply, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, congr_mk, quotientKerEquivOfRightInverse_symm_apply
hasNeg 📖	CompOp	—
hasSub 📖	CompOp	—
hrecOn₂ 📖	CompOp	1 math math: hrec_on₂_coe
instCoeTCQuotient 📖	CompOp	—
instCompleteLattice 📖	CompOp	10 math math: sSup_eq_addConGen, sup_def, toSetoid_top, toSetoid_bot, inf_iff_and, sSup_def, sup_eq_addConGen, toSetoid_eq_bot, toSetoid_eq_top, coe_inf
instDecidableEqQuotientOfDecidableCoeForallProp 📖	CompOp	—
instFunLikeForallProp 📖	CompOp	32 math math: sSup_eq_addConGen, eq, sup_def, liftOnAddUnits_mk, coe_inj, coe_iInf, addConGen_idem, addConGen_of_addCon, AddLocalization.r_of_eq, ker_rel, inf_iff_and, quot_mk_eq_coe, rel_mk, le_def, mem_addSubgroup_iff, AddLocalization.r_iff_exists, AddLocalization.zero_rel, coe_sInf, ker_apply, AddSubmonoid.LocalizationMap.eq', AddLocalization.mk_eq_mk_iff, rel_eq_coe, sSup_def, AddMonoid.Coprod.mk_eq_mk, comap_rel, sup_eq_addConGen, ext_iff, map_apply, AddLocalization.r_iff_oreEqv_r, refl, coe_inf, AddMonoid.Coprod.con_neg_add_cancel
instInfSet 📖	CompOp	4 math math: coe_iInf, coe_sInf, addConGen_eq, sInf_toSetoid
instInhabited 📖	CompOp	—
instLE 📖	CompOp	11 math math: le_iff, le_def, AddSubgroup.orderIsoAddCon_symm_apply_coe, addConGen_mono, AddSubgroup.orderIsoAddCon_apply, orderIsoOp_apply, addConGen_le, QuotientAddGroup.con_mono, le_comap_conGen, orderIsoOp_symm_apply, QuotientAddGroup.con_le_iff
instMembershipProd 📖	CompOp	1 math math: mem_coe
instPartialOrder 📖	CompOp	—
liftOn 📖	CompOp	2 math math: liftOn_coe, CharacterModule.homEquiv_apply_apply
liftOnAddUnits 📖	CompOp	1 math math: liftOnAddUnits_mk
liftOn₂ 📖	CompOp	—
toQuotient 📖	CompOp	17 math math: eq, FreeAddMonoid.toPiTensorProduct, quot_mk_eq_coe, comapQuotientEquivOfSurj_symm_mk, coe_add, coe_mk', coe_vadd, kerLift_mk, mkAddHom_apply, liftOn_coe, map_apply, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, lift_coe, coe_zero, congr_mk, quotientKerEquivOfRightInverse_symm_apply
toSetoid 📖	CompOp	10 math math: toSetoid_top, toSetoid_bot, Module.DirectLimit.quotMk_of, rel_eq_coe, toSetoid_injective, toSetoid_eq_bot, comapQuotientEquivOfSurj_symm_mk', toSetoid_inj, sInf_toSetoid, toSetoid_eq_top
zero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	DFunLike.coe AddCon instFunLikeForallProp	—	—	add'
add' 📖	—	toSetoid	—	—	—
addConGen_eq 📖	mathematical	—	addConGen InfSet.sInf AddCon instInfSet setOf	—	le_antisymm le_sInf Setoid.refl' Setoid.symm' Setoid.trans' add sInf_le
addConGen_idem 📖	mathematical	—	addConGen DFunLike.coe AddCon instFunLikeForallProp	—	addConGen_of_addCon
addConGen_le 📖	mathematical	DFunLike.coe AddCon instFunLikeForallProp	instLE addConGen	—	addConGen_eq sInf_le
addConGen_mono 📖	mathematical	—	AddCon instLE addConGen	—	addConGen_le
addConGen_of_addCon 📖	mathematical	—	addConGen DFunLike.coe AddCon instFunLikeForallProp	—	le_antisymm addConGen_eq sInf_le
coe_add 📖	mathematical	—	toQuotient Quotient hasAdd	—	—
coe_iInf 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp iInf instInfSet Pi.infSet CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Prop.instCompleteLattice	—	iInf.eq_1 coe_sInf Set.range_comp sInf_range
coe_inf 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice Pi.instMinForall_mathlib Prop.instCompleteLattice	—	—
coe_inj 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp	—	DFunLike.coe_injective
coe_sInf 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp InfSet.sInf instInfSet Pi.infSet CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Prop.instCompleteLattice Set.image	—	sInf_image iInf_apply iInf_Prop_eq
coe_zero 📖	mathematical	—	toQuotient AddZero.toAdd AddZeroClass.toAddZero AddZero.toZero Quotient addZeroClass	—	—
comap_rel 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp comap	—	—
eq 📖	mathematical	—	toQuotient DFunLike.coe AddCon instFunLikeForallProp	—	Quotient.eq''
ext 📖	—	DFunLike.coe AddCon instFunLikeForallProp	—	—	ext'
ext' 📖	—	DFunLike.coe AddCon instFunLikeForallProp	—	—	DFunLike.coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp	—	ext
hrec_on₂_coe 📖	mathematical	toQuotient	hrecOn₂	—	—
induction_on 📖	—	toQuotient	—	—	Quotient.inductionOn'
induction_on_addUnits 📖	—	Quotient AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass addMonoid toQuotient AddZero.toZero DFunLike.coe AddCon instFunLikeForallProp eq	—	—	eq
induction_on₂ 📖	—	toQuotient	—	—	Quotient.inductionOn₂'
inf_iff_and 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice	—	—
le_def 📖	mathematical	—	AddCon instLE DFunLike.coe instFunLikeForallProp	—	—
liftOnAddUnits_mk 📖	mathematical	Quotient AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass addMonoid toQuotient AddZero.toZero	liftOnAddUnits DFunLike.coe AddCon instFunLikeForallProp eq	—	—
liftOn_coe 📖	mathematical	—	liftOn toQuotient	—	—
map_of_add_left_rel_zero 📖	—	DFunLike.coe AddCon AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLikeForallProp AddZero.toZero	—	—	eq zero_add add_assoc add_zero AddUnits.ext
neg 📖	mathematical	DFunLike.coe AddCon AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLikeForallProp	SubNegMonoid.toNeg	—	map_of_add_left_rel_zero neg_add_cancel refl
nsmul 📖	mathematical	DFunLike.coe AddCon AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLikeForallProp	AddMonoid.toNatSMul	—	zero_nsmul refl succ_nsmul add
quot_mk_eq_coe 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp toQuotient	—	—
refl 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp	—	Setoid.refl'
rel_eq_coe 📖	mathematical	—	toSetoid DFunLike.coe AddCon instFunLikeForallProp	—	—
rel_mk 📖	mathematical	—	DFunLike.coe AddCon instFunLikeForallProp	—	—
sInf_toSetoid 📖	mathematical	—	toSetoid InfSet.sInf AddCon instInfSet Setoid.instInfSet Set.image	—	Setoid.ext
sSup_def 📖	mathematical	—	SupSet.sSup AddCon CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice addConGen Pi.supSet Prop.instCompleteLattice Set.image DFunLike.coe instFunLikeForallProp	—	sSup_eq_addConGen sSup_image iSup_apply iSup_Prop_eq
sSup_eq_addConGen 📖	mathematical	—	SupSet.sSup AddCon CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice addConGen Set Set.instMembership DFunLike.coe instFunLikeForallProp	—	addConGen_eq Set.ext
sub 📖	mathematical	DFunLike.coe AddCon AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLikeForallProp	SubNegMonoid.toSub	—	sub_eq_add_neg add neg
sup_def 📖	mathematical	—	AddCon SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice addConGen Pi.instMaxForall_mathlib Prop.instCompleteLattice DFunLike.coe instFunLikeForallProp	—	sup_eq_addConGen
sup_eq_addConGen 📖	mathematical	—	AddCon SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice addConGen DFunLike.coe instFunLikeForallProp	—	addConGen_eq le_def
toSetoid_bot 📖	mathematical	—	toSetoid Bot.bot AddCon OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Setoid.completeLattice	—	—
toSetoid_eq_bot 📖	mathematical	—	toSetoid Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Setoid.completeLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder AddCon instCompleteLattice	—	toSetoid_bot
toSetoid_eq_top 📖	mathematical	—	toSetoid Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Setoid.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AddCon instCompleteLattice	—	toSetoid_top
toSetoid_inj 📖	mathematical	—	toSetoid	—	toSetoid_injective
toSetoid_injective 📖	mathematical	—	AddCon toSetoid	—	add'
toSetoid_top 📖	mathematical	—	toSetoid Top.top AddCon OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Setoid.completeLattice	—	—
trans 📖	—	DFunLike.coe AddCon instFunLikeForallProp	—	—	Setoid.trans'
zsmul 📖	mathematical	DFunLike.coe AddCon AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLikeForallProp	SubNegMonoid.toZSMul	—	natCast_zsmul nsmul negSucc_zsmul neg

AddCon.Quotient

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—
nsmul 📖	CompOp	—
zsmul 📖	CompOp	—

Con

Definitions

Name	Category	Theorems
comap 📖	CompOp	8 math math: comap_conGen_of_bijective, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, comapQuotientEquivOfSurj_symm_mk, comap_eq, le_comap_conGen, comap_conGen_equiv, comap_rel
commGroup 📖	CompOp	—
commMagma 📖	CompOp	—
commMonoid 📖	CompOp	—
commSemigroup 📖	CompOp	—
gi 📖	CompOp	—
group 📖	CompOp	—
hasDiv 📖	CompOp	—
hasInv 📖	CompOp	—
hasMul 📖	CompOp	9 math math: mkMulHom_apply, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, quotientKerEquivOfRightInverse_symm_apply, comapQuotientEquivOfSurj_symm_mk, quotientKerEquivOfRightInverse_apply, congr_mk, coe_mul, ker_mkMulHom_eq
hrecOn₂ 📖	CompOp	1 math math: hrec_on₂_coe
instCoeTCQuotient 📖	CompOp	—
instCompleteLattice 📖	CompOp	14 math math: RingCon.toCon_eq_bot, sup_eq_conGen, coe_inf, toSetoid_eq_bot, sSup_eq_conGen, sup_def, toSetoid_bot, inf_iff_and, sSup_def, RingCon.toCon_eq_top, toSetoid_top, toSetoid_eq_top, RingCon.toCon_bot, RingCon.toCon_top
instDecidableEqQuotientOfDecidableCoeForallProp 📖	CompOp	—
instFunLikeForallProp 📖	CompOp	35 math math: Localization.one_rel, liftOnUnits_mk, RingCon.rel_mk, sup_eq_conGen, ker_rel, conGen_idem, refl, ker_apply, coe_inf, Monoid.Coprod.con_inv_mul_cancel, mem_subgroup_iff, rel_mk, Localization.r_of_eq, coe_iInf, eq, rel_eq_coe, sSup_eq_conGen, coe_inj, sup_def, Localization.r_iff_exists, RingCon.coe_mk, conGen_of_con, le_def, Submonoid.LocalizationMap.eq', inf_iff_and, coe_sInf, sSup_def, map_apply, Localization.r_iff_oreEqv_r, quot_mk_eq_coe, RingCon.toCon_coe_eq_coe, Monoid.Coprod.mk_eq_mk, comap_rel, ext_iff, Localization.mk_eq_mk_iff
instInfSet 📖	CompOp	4 math math: sInf_toSetoid, conGen_eq, coe_iInf, coe_sInf
instInhabited 📖	CompOp	—
instLE 📖	CompOp	11 math math: le_iff, QuotientGroup.con_le_iff, orderIsoOp_symm_apply, conGen_le, Subgroup.orderIsoCon_apply, conGen_mono, orderIsoOp_apply, le_def, Subgroup.orderIsoCon_symm_apply_coe, QuotientGroup.con_mono, le_comap_conGen
instMembershipProd 📖	CompOp	1 math math: mem_coe
instPartialOrder 📖	CompOp	—
instPowQuotientNat 📖	CompOp	—
liftOn 📖	CompOp	1 math math: liftOn_coe
liftOnUnits 📖	CompOp	1 math math: liftOnUnits_mk
liftOn₂ 📖	CompOp	—
monoid 📖	CompOp	—
mulOneClass 📖	CompOp	19 math math: hom_ext_iff, lift_surjective_of_surjective, mk'_surjective, kerLift_mk, lift_comp_mk', Monoid.CoprodI.of_apply, kerLift_range_eq, quotientKerEquivOfRightInverse_apply, comap_eq, coe_mk', coe_one, lift_mk', lift_coe, lift_apply_mk', mk'_ker, lift_range, map_apply, kerLift_injective, mrange_mk'
one 📖	CompOp	—
semigroup 📖	CompOp	—
toQuotient 📖	CompOp	16 math math: mkMulHom_apply, kerLift_mk, comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_mk, liftOn_coe, eq, quotientKerEquivOfRightInverse_symm_apply, comapQuotientEquivOfSurj_symm_mk, coe_smul, coe_mk', coe_one, congr_mk, lift_coe, coe_mul, map_apply, quot_mk_eq_coe
toSetoid 📖	CompOp	19 math math: TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, sInf_toSetoid, RingCon.comapQuotientEquivOfSurj_symm_mk', comapQuotientEquivOfSurj_symm_mk', RingCon.sInf_toSetoid, RingCon.factorₐ_mk, toSetoid_eq_bot, rel_eq_coe, RingCon.quotientQuotientEquivQuotientₐ_mk_mk, toSetoid_inj, RingCon.quotientQuotientEquivQuotient_mk_mk, toSetoid_bot, RingCon.quotientQuotientEquivQuotientₐ_symm_mk, TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r, toSetoid_injective, toSetoid_top, RingCon.rel_eq_coe, RingCon.quotientQuotientEquivQuotient_symm_mk, toSetoid_eq_top
zpowinst 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_iInf 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp iInf instInfSet Pi.infSet CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Prop.instCompleteLattice	—	iInf.eq_1 coe_sInf Set.range_comp sInf_range
coe_inf 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice Pi.instMinForall_mathlib Prop.instCompleteLattice	—	—
coe_inj 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp	—	DFunLike.coe_injective
coe_mul 📖	mathematical	—	toQuotient Quotient hasMul	—	—
coe_one 📖	mathematical	—	toQuotient MulOne.toMul MulOneClass.toMulOne MulOne.toOne Quotient mulOneClass	—	—
coe_sInf 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp InfSet.sInf instInfSet Pi.infSet CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Prop.instCompleteLattice Set.image	—	sInf_image iInf_apply iInf_Prop_eq
comap_rel 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp comap	—	—
conGen_eq 📖	mathematical	—	conGen InfSet.sInf Con instInfSet setOf	—	le_antisymm le_sInf Setoid.refl' Setoid.symm' Setoid.trans' mul sInf_le
conGen_idem 📖	mathematical	—	conGen DFunLike.coe Con instFunLikeForallProp	—	conGen_of_con
conGen_le 📖	mathematical	DFunLike.coe Con instFunLikeForallProp	instLE conGen	—	conGen_eq sInf_le
conGen_mono 📖	mathematical	—	Con instLE conGen	—	conGen_le
conGen_of_con 📖	mathematical	—	conGen DFunLike.coe Con instFunLikeForallProp	—	le_antisymm conGen_eq sInf_le
div 📖	mathematical	DFunLike.coe Con MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLikeForallProp	DivInvMonoid.toDiv	—	div_eq_mul_inv mul inv
eq 📖	mathematical	—	toQuotient DFunLike.coe Con instFunLikeForallProp	—	Quotient.eq''
ext 📖	—	DFunLike.coe Con instFunLikeForallProp	—	—	ext'
ext' 📖	—	DFunLike.coe Con instFunLikeForallProp	—	—	DFunLike.coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp	—	ext
hrec_on₂_coe 📖	mathematical	toQuotient	hrecOn₂	—	—
induction_on 📖	—	toQuotient	—	—	Quotient.inductionOn'
induction_on_units 📖	—	Quotient MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass monoid toQuotient MulOne.toOne DFunLike.coe Con instFunLikeForallProp eq	—	—	eq
induction_on₂ 📖	—	toQuotient	—	—	Quotient.inductionOn₂'
inf_iff_and 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice	—	—
inv 📖	mathematical	DFunLike.coe Con MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLikeForallProp	DivInvMonoid.toInv	—	map_of_mul_left_rel_one inv_mul_cancel refl
le_def 📖	mathematical	—	Con instLE DFunLike.coe instFunLikeForallProp	—	—
liftOnUnits_mk 📖	mathematical	Quotient MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass monoid toQuotient MulOne.toOne	liftOnUnits DFunLike.coe Con instFunLikeForallProp eq	—	—
liftOn_coe 📖	mathematical	—	liftOn toQuotient	—	—
map_of_mul_left_rel_one 📖	—	DFunLike.coe Con MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instFunLikeForallProp MulOne.toOne	—	—	one_mul mul_assoc mul_one Units.ext
mul 📖	—	DFunLike.coe Con instFunLikeForallProp	—	—	mul'
mul' 📖	—	toSetoid	—	—	—
pow 📖	mathematical	DFunLike.coe Con MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instFunLikeForallProp	Monoid.toNatPow	—	pow_zero refl pow_succ mul
quot_mk_eq_coe 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp toQuotient	—	—
refl 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp	—	Setoid.refl'
rel_eq_coe 📖	mathematical	—	toSetoid DFunLike.coe Con instFunLikeForallProp	—	—
rel_mk 📖	mathematical	—	DFunLike.coe Con instFunLikeForallProp	—	—
sInf_toSetoid 📖	mathematical	—	toSetoid InfSet.sInf Con instInfSet Setoid.instInfSet Set.image	—	Setoid.ext
sSup_def 📖	mathematical	—	SupSet.sSup Con CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice conGen Pi.supSet Prop.instCompleteLattice Set.image DFunLike.coe instFunLikeForallProp	—	sSup_eq_conGen sSup_image iSup_apply iSup_Prop_eq
sSup_eq_conGen 📖	mathematical	—	SupSet.sSup Con CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice conGen Set Set.instMembership DFunLike.coe instFunLikeForallProp	—	conGen_eq Set.ext
sup_def 📖	mathematical	—	Con SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice conGen Pi.instMaxForall_mathlib Prop.instCompleteLattice DFunLike.coe instFunLikeForallProp	—	sup_eq_conGen
sup_eq_conGen 📖	mathematical	—	Con SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice conGen DFunLike.coe instFunLikeForallProp	—	conGen_eq
toSetoid_bot 📖	mathematical	—	toSetoid Bot.bot Con OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Setoid.completeLattice	—	—
toSetoid_eq_bot 📖	mathematical	—	toSetoid Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Setoid.completeLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Con instCompleteLattice	—	toSetoid_bot
toSetoid_eq_top 📖	mathematical	—	toSetoid Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Setoid.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Con instCompleteLattice	—	toSetoid_top
toSetoid_inj 📖	mathematical	—	toSetoid	—	toSetoid_injective
toSetoid_injective 📖	mathematical	—	Con toSetoid	—	mul'
toSetoid_top 📖	mathematical	—	toSetoid Top.top Con OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Setoid.completeLattice	—	—
trans 📖	—	DFunLike.coe Con instFunLikeForallProp	—	—	Setoid.trans'
zpow 📖	mathematical	DFunLike.coe Con MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLikeForallProp	DivInvMonoid.toZPow	—	zpow_natCast pow zpow_negSucc inv

Con.Quotient

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
AddCon 📖	CompData	48 math math: AddCon.sSup_eq_addConGen, AddCon.eq, AddCon.sup_def, AddCon.toSetoid_top, AddCon.liftOnAddUnits_mk, AddCon.coe_inj, AddCon.toSetoid_bot, AddCon.coe_iInf, AddCon.addConGen_idem, AddCon.addConGen_of_addCon, AddCon.le_iff, AddLocalization.r_of_eq, AddCon.ker_rel, AddCon.inf_iff_and, AddCon.quot_mk_eq_coe, AddCon.rel_mk, AddCon.le_def, AddCon.mem_addSubgroup_iff, AddLocalization.r_iff_exists, AddSubgroup.orderIsoAddCon_symm_apply_coe, AddLocalization.zero_rel, AddCon.coe_sInf, AddCon.ker_apply, AddSubmonoid.LocalizationMap.eq', AddLocalization.mk_eq_mk_iff, AddCon.rel_eq_coe, AddCon.sSup_def, AddMonoid.Coprod.mk_eq_mk, AddCon.comap_rel, AddCon.sup_eq_addConGen, AddCon.addConGen_mono, AddCon.addConGen_eq, AddSubgroup.orderIsoAddCon_apply, AddCon.orderIsoOp_apply, AddCon.toSetoid_injective, AddCon.ext_iff, AddLocalization.r_iff_oreEqv_r, AddCon.toSetoid_eq_bot, QuotientAddGroup.con_mono, AddCon.le_comap_conGen, AddCon.orderIsoOp_symm_apply, QuotientAddGroup.con_le_iff, AddCon.sInf_toSetoid, AddCon.toSetoid_eq_top, AddCon.mem_coe, AddCon.refl, AddCon.coe_inf, AddMonoid.Coprod.con_neg_add_cancel
Con 📖	CompData	56 math math: Localization.one_rel, RingCon.toCon_eq_bot, Con.liftOnUnits_mk, RingCon.rel_mk, Con.le_iff, Con.sup_eq_conGen, RingCon.toCon_injective, Con.ker_rel, Con.conGen_idem, Con.refl, Con.sInf_toSetoid, Con.ker_apply, QuotientGroup.con_le_iff, Con.coe_inf, Monoid.Coprod.con_inv_mul_cancel, Con.mem_subgroup_iff, Con.rel_mk, Con.mem_coe, Con.conGen_eq, Con.orderIsoOp_symm_apply, Localization.r_of_eq, Con.toSetoid_eq_bot, Subgroup.orderIsoCon_apply, Con.coe_iInf, Con.eq, Con.rel_eq_coe, Con.sSup_eq_conGen, Con.coe_inj, Con.sup_def, Localization.r_iff_exists, Con.conGen_mono, Con.toSetoid_bot, RingCon.coe_mk, Con.orderIsoOp_apply, Con.conGen_of_con, Con.le_def, Submonoid.LocalizationMap.eq', Con.toSetoid_injective, Subgroup.orderIsoCon_symm_apply_coe, QuotientGroup.con_mono, Con.le_comap_conGen, Con.inf_iff_and, Con.coe_sInf, Con.sSup_def, RingCon.toCon_eq_top, Con.toSetoid_top, Localization.r_iff_oreEqv_r, Con.toSetoid_eq_top, Con.quot_mk_eq_coe, RingCon.toCon_coe_eq_coe, Monoid.Coprod.mk_eq_mk, Con.comap_rel, RingCon.toCon_bot, RingCon.toCon_top, Con.ext_iff, Localization.mk_eq_mk_iff
addConGen 📖	CompOp	14 math math: AddCon.sSup_eq_addConGen, FreeAddMonoid.toPiTensorProduct, AddCon.sup_def, AddCon.addConGen_idem, AddCon.addConGen_of_addCon, AddCon.comap_conGen_equiv, AddCon.sSup_def, AddCon.sup_eq_addConGen, AddCon.addConGen_mono, AddCon.addConGen_eq, AddCon.addConGen_le, AddCon.comap_conGen_of_bijective, AddCon.le_comap_conGen, CharacterModule.homEquiv_apply_apply
conGen 📖	CompOp	13 math math: Con.sup_eq_conGen, Con.conGen_idem, Con.comap_conGen_of_bijective, Con.conGen_eq, Con.conGen_le, Monoid.CoprodI.of_apply, Con.sSup_eq_conGen, Con.sup_def, Con.conGen_mono, Con.conGen_of_con, Con.le_comap_conGen, Con.sSup_def, Con.comap_conGen_equiv

---

← Back to Index