Basic

📁 Source: Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

Statistics

Metric	Count
Definitions TwoSidedIdeal, addCommGroup, coeAddMonoidHom, coeOrderEmbedding, instAddSubtypeMem, instNegSubtypeMem, instPartialOrder, instSMulIntSubtypeMem, instSMulNatSubtypeMem, instSubSubtypeMem, instZeroSubtypeMem, mk', op, opOrderIso, orderIsoRingCon, ringCon, setLike, unop	18
Theorems add_mem, coeAddMonoidHom_apply, coeOrderEmbedding_apply, coe_mk, coe_mk', coe_op, coe_unop, ext, ext_iff, instAddSubgroupClass, instNontrivial, instSMulMemClass, instSMulMemClassMulOpposite, le_iff, lt_iff, mem_iff, mem_mk, mem_mk', mem_op_iff, mem_unop_iff, mul_mem_left, mul_mem_right, neg_mem, nsmul_mem, opOrderIso_apply, opOrderIso_symm_apply, op_ringCon, orderIsoRingCon_apply, orderIsoRingCon_symm_apply, rel_iff, ringCon_injective, ringCon_le_iff, sub_mem, unop_ringCon, zero_mem, zsmul_mem	36
Total	54

TwoSidedIdeal

Definitions

Name	Category	Theorems
addCommGroup 📖	CompOp	6 math math: subtype_injective, coe_subtype, subtypeMop_apply, coeAddMonoidHom_apply, subtypeMop_injective, subtype_apply
coeAddMonoidHom 📖	CompOp	1 math math: coeAddMonoidHom_apply
coeOrderEmbedding 📖	CompOp	1 math math: coeOrderEmbedding_apply
instAddSubtypeMem 📖	CompOp	—
instNegSubtypeMem 📖	CompOp	—
instPartialOrder 📖	CompOp	36 math math: orderIsoRingCon_symm_apply, ringCon_le_iff, Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, span_mono, orderIsoRingCon_apply, MvPowerSeries.LinearTopology.basis_le_iff, instIsTwoSidedCoeOrderHomIdealAsIdeal, bot_asIdeal, orderIsoMatrix_apply_ringCon_r, Ideal.toTwoSided_asIdeal, orderIsoIsTwoSided_symm_apply, opOrderIso_symm_apply, RingEquiv.mapTwoSidedIdeal_symm, isSimpleRing_iff, asIdeal_jacobson, mem_fromIdeal, opOrderIso_apply, mem_comap, mem_asIdealOpposite, RingEquiv.mapTwoSidedIdeal_apply, le_iff, comap_comap, IsSimpleRing.simple, top_asIdeal, mem_asIdeal, Ideal.asIdeal_toTwoSided, orderIsoMatrix_symm_apply_ringCon_r, span_le, gc, matrix_monotone, coeOrderEmbedding_apply, lt_iff, orderIsoIsTwoSided_apply_coe, asIdeal_matrix, matrix_strictMono_of_nonempty, coe_asIdeal
instSMulIntSubtypeMem 📖	CompOp	—
instSMulNatSubtypeMem 📖	CompOp	—
instSubSubtypeMem 📖	CompOp	—
instZeroSubtypeMem 📖	CompOp	—
mk' 📖	CompOp	2 math math: coe_mk', mem_mk'
op 📖	CompOp	4 math math: mem_op_iff, opOrderIso_apply, op_ringCon, coe_op
opOrderIso 📖	CompOp	2 math math: opOrderIso_symm_apply, opOrderIso_apply
orderIsoRingCon 📖	CompOp	2 math math: orderIsoRingCon_symm_apply, orderIsoRingCon_apply
ringCon 📖	CompOp	21 math math: ringCon_injective, ringCon_le_iff, orderIsoRingCon_apply, equivMatrix_symm_apply_ringCon, iSup_ringCon, iInf_ringCon, orderIsoMatrix_apply_ringCon_r, ker_ringCon, sInf_ringCon, op_ringCon, sSup_ringCon, rel_iff, orderIsoMatrix_symm_apply_ringCon_r, mem_iff, top_ringCon, sup_ringCon, bot_ringCon, matrix_ringCon, ker_ringCon_mk', inf_ringCon, unop_ringCon
setLike 📖	CompOp	64 math math: mem_span_iff_mem_addSubgroup_closure_absorbing, one_mem_iff, instSMulCommClassMulOppositeSubtypeMem, one_mem, mem_span_iff_mem_addSubgroup_closure, mem_iInf, coe_top, isLinearTopology_iff_hasBasis_open_twoSidedIdeal, Ideal.mem_toTwoSided, mem_mk, mem_op_iff, MvPowerSeries.LinearTopology.mem_basis_iff, mem_matrix, IsLinearTopology.hasBasis_twoSidedIdeal, mem_inf, coe_mk', instNonUnitalSubringClassTwoSidedIdeal, mem_jacobson_iff, mem_fromIdeal, mem_comap, mem_asIdealOpposite, instSMulMemClass, IsSimpleRing.one_mem_of_ne_bot, mem_top, le_iff, subtype_injective, coe_equivMatrix_symm_apply, mem_compactlySupported, Ideal.coe_toTwoSided, coe_bot, ofCompactSupport_mem, mem_span_iff_mem_addSubgroup_closure_nonunital, rel_iff, mem_span_iff, coe_mk, mem_asIdeal, mem_sup, mem_iff, coe_subtype, span_le, ext_iff, subset_span, subtypeMop_apply, coeOrderEmbedding_apply, coeAddMonoidHom_apply, lt_iff, mem_ker, coe_unop, instSMulMemClassMulOpposite, coe_op, subtypeMop_injective, coe_smul, mem_unop_iff, isLinearTopology_iff_hasBasis_twoSidedIdeal, MvPowerSeries.LinearTopology.hasBasis_nhds_zero, subtype_apply, zero_mem, IsLinearTopology.hasBasis_open_twoSidedIdeal, coe_asIdeal, mem_mk', mem_bot, instAddSubgroupClass, coe_mop_smul, mem_sInf
unop 📖	CompOp	4 math math: opOrderIso_symm_apply, coe_unop, mem_unop_iff, unop_ringCon

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	add_zero RingCon.add
coeAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom TwoSidedIdeal SetLike.instMembership setLike AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup addCommGroup NonUnitalNonAssocRing.toAddCommGroup AddMonoidHom.instFunLike coeAddMonoidHom	—	—
coeOrderEmbedding_apply 📖	mathematical	—	DFunLike.coe RelEmbedding TwoSidedIdeal Set Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.instLE RelEmbedding.instFunLike coeOrderEmbedding SetLike.coe setLike	—	—
coe_mk 📖	mathematical	—	SetLike.coe TwoSidedIdeal setLike setOf DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul RingCon.instFunLikeForallProp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
coe_mk' 📖	mathematical	Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup Distrib.toMul	SetLike.coe TwoSidedIdeal setLike mk'	—	Set.ext mem_mk'
coe_op 📖	mathematical	—	SetLike.coe TwoSidedIdeal MulOpposite MulOpposite.instNonUnitalNonAssocRing setLike op Set.preimage MulOpposite.unop	—	Set.ext mem_op_iff
coe_unop 📖	mathematical	—	SetLike.coe TwoSidedIdeal setLike unop Set.preimage MulOpposite MulOpposite.op MulOpposite.instNonUnitalNonAssocRing	—	Set.ext mem_unop_iff
ext 📖	—	TwoSidedIdeal SetLike.instMembership setLike	—	—	RelEmbedding.injective Set.ext
ext_iff 📖	mathematical	—	TwoSidedIdeal SetLike.instMembership setLike	—	ext
instAddSubgroupClass 📖	mathematical	—	AddSubgroupClass TwoSidedIdeal AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup setLike	—	add_mem zero_mem neg_mem
instNontrivial 📖	mathematical	—	Nontrivial TwoSidedIdeal	—	RingCon.instNontrivial Mathlib.Tactic.Contrapose.contrapose₄
instSMulMemClass 📖	mathematical	—	SMulMemClass TwoSidedIdeal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring setLike	—	mul_mem_left
instSMulMemClassMulOpposite 📖	mathematical	—	SMulMemClass TwoSidedIdeal MulOpposite SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring SMulWithZero.toSMulZeroClass MulOpposite.instZero MulZeroClass.toOppositeSMulWithZero setLike	—	mul_mem_right
le_iff 📖	mathematical	—	TwoSidedIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Set.instHasSubset SetLike.coe setLike	—	—
lt_iff 📖	mathematical	—	TwoSidedIdeal Preorder.toLT PartialOrder.toPreorder instPartialOrder Set Set.instHasSSubset SetLike.coe setLike	—	lt_iff_le_and_ne Set.ssubset_iff_subset_ne le_iff instIsConcreteLE
mem_iff 📖	mathematical	—	TwoSidedIdeal SetLike.instMembership setLike DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul RingCon.instFunLikeForallProp ringCon MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
mem_mk 📖	mathematical	—	TwoSidedIdeal SetLike.instMembership setLike DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul RingCon.instFunLikeForallProp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
mem_mk' 📖	mathematical	Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup Distrib.toMul	TwoSidedIdeal SetLike.instMembership setLike mk'	—	mem_iff sub_zero
mem_op_iff 📖	mathematical	—	MulOpposite TwoSidedIdeal MulOpposite.instNonUnitalNonAssocRing SetLike.instMembership setLike op MulOpposite.unop	—	Setoid.comm'
mem_unop_iff 📖	mathematical	—	TwoSidedIdeal SetLike.instMembership setLike unop MulOpposite MulOpposite.instNonUnitalNonAssocRing MulOpposite.op	—	Setoid.comm'
mul_mem_left 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	MulZeroClass.mul_zero RingCon.mul RingCon.refl
mul_mem_right 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	MulZeroClass.zero_mul RingCon.mul RingCon.refl
neg_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup	—	neg_zero RingCon.neg
nsmul_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	nsmul_mem AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass
opOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso TwoSidedIdeal MulOpposite MulOpposite.instNonUnitalNonAssocRing Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike opOrderIso op	—	—
opOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe RelIso TwoSidedIdeal MulOpposite MulOpposite.instNonUnitalNonAssocRing Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike RelIso.symm opOrderIso unop	—	—
op_ringCon 📖	mathematical	—	ringCon MulOpposite MulOpposite.instNonUnitalNonAssocRing op RingCon.op Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul	—	—
orderIsoRingCon_apply 📖	mathematical	—	DFunLike.coe RelIso TwoSidedIdeal RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul Preorder.toLE PartialOrder.toPreorder instPartialOrder RingCon.instLE RelIso.instFunLike orderIsoRingCon ringCon	—	—
orderIsoRingCon_symm_apply 📖	mathematical	—	DFunLike.coe RelIso RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul TwoSidedIdeal RingCon.instLE Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike RelIso.symm orderIsoRingCon	—	—
rel_iff 📖	mathematical	—	DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul RingCon.instFunLikeForallProp ringCon TwoSidedIdeal SetLike.instMembership setLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	mem_iff Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg zero_add Mathlib.Tactic.Abel.zero_termg RingCon.sub RingCon.refl Mathlib.Tactic.Abel.term_add_constg RingCon.add
ringCon_injective 📖	mathematical	—	TwoSidedIdeal RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul ringCon	—	—
ringCon_le_iff 📖	mathematical	—	TwoSidedIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul RingCon.instLE ringCon	—	RelIso.map_rel_iff
sub_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	sub_mem instAddSubgroupClass
unop_ringCon 📖	mathematical	—	ringCon unop RingCon.unop AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring MulOpposite MulOpposite.instNonUnitalNonAssocRing	—	—
zero_mem 📖	mathematical	—	TwoSidedIdeal SetLike.instMembership setLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	RingCon.refl
zsmul_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	zsmul_mem instAddSubgroupClass

(root)

Definitions

Name	Category	Theorems
TwoSidedIdeal 📖	CompData	109 math math: TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing, TwoSidedIdeal.orderIsoRingCon_symm_apply, TwoSidedIdeal.ringCon_injective, TwoSidedIdeal.one_mem_iff, TwoSidedIdeal.instSMulCommClassMulOppositeSubtypeMem, TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure, TwoSidedIdeal.mem_iInf, TwoSidedIdeal.ringCon_le_iff, Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, TwoSidedIdeal.span_mono, TwoSidedIdeal.orderIsoRingCon_apply, TwoSidedIdeal.equivMatrix_symm_apply_ringCon, TwoSidedIdeal.matrix_jacobson_bot, TwoSidedIdeal.coe_top, MvPowerSeries.LinearTopology.basis_le_iff, isLinearTopology_iff_hasBasis_open_twoSidedIdeal, Ideal.mem_toTwoSided, TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal, TwoSidedIdeal.iSup_ringCon, TwoSidedIdeal.mem_mk, TwoSidedIdeal.iInf_ringCon, TwoSidedIdeal.bot_asIdeal, compactlySupported_eq_top_of_isCompact, TwoSidedIdeal.equivMatrix_apply, TwoSidedIdeal.matrix_top, TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, Ideal.toTwoSided_asIdeal, TwoSidedIdeal.mem_op_iff, MvPowerSeries.LinearTopology.mem_basis_iff, TwoSidedIdeal.matrix_bot, TwoSidedIdeal.mem_matrix, IsLinearTopology.hasBasis_twoSidedIdeal, TwoSidedIdeal.orderIsoIsTwoSided_symm_apply, TwoSidedIdeal.mem_inf, TwoSidedIdeal.opOrderIso_symm_apply, TwoSidedIdeal.coe_mk', TwoSidedIdeal.instNontrivial, compactlySupported_eq_top, TwoSidedIdeal.ker_eq_bot, TwoSidedIdeal.sInf_ringCon, RingEquiv.mapTwoSidedIdeal_symm, instNonUnitalSubringClassTwoSidedIdeal, TwoSidedIdeal.mem_jacobson_iff, compactlySupported_eq_top_iff, isSimpleRing_iff, TwoSidedIdeal.asIdeal_jacobson, TwoSidedIdeal.mem_fromIdeal, TwoSidedIdeal.opOrderIso_apply, TwoSidedIdeal.mem_comap, TwoSidedIdeal.mem_asIdealOpposite, TwoSidedIdeal.instSMulMemClass, IsSimpleRing.one_mem_of_ne_bot, TwoSidedIdeal.mem_top, RingEquiv.mapTwoSidedIdeal_apply, TwoSidedIdeal.le_iff, TwoSidedIdeal.subtype_injective, TwoSidedIdeal.coe_equivMatrix_symm_apply, mem_compactlySupported, Ideal.coe_toTwoSided, TwoSidedIdeal.coe_bot, TwoSidedIdeal.sSup_ringCon, ofCompactSupport_mem, TwoSidedIdeal.comap_comap, IsSimpleRing.simple, TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital, TwoSidedIdeal.rel_iff, TwoSidedIdeal.mem_span_iff, TwoSidedIdeal.coe_mk, TwoSidedIdeal.top_asIdeal, TwoSidedIdeal.mem_asIdeal, Ideal.asIdeal_toTwoSided, TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r, TwoSidedIdeal.mem_sup, TwoSidedIdeal.mem_iff, TwoSidedIdeal.top_ringCon, TwoSidedIdeal.coe_subtype, TwoSidedIdeal.sup_ringCon, TwoSidedIdeal.span_le, TwoSidedIdeal.ext_iff, TwoSidedIdeal.gc, TwoSidedIdeal.matrix_monotone, TwoSidedIdeal.subset_span, TwoSidedIdeal.subtypeMop_apply, TwoSidedIdeal.coeOrderEmbedding_apply, TwoSidedIdeal.coeAddMonoidHom_apply, TwoSidedIdeal.lt_iff, TwoSidedIdeal.mem_ker, TwoSidedIdeal.bot_ringCon, TwoSidedIdeal.coe_unop, TwoSidedIdeal.orderIsoIsTwoSided_apply_coe, TwoSidedIdeal.asIdeal_matrix, TwoSidedIdeal.instSMulMemClassMulOpposite, TwoSidedIdeal.coe_op, TwoSidedIdeal.subtypeMop_injective, TwoSidedIdeal.coe_smul, TwoSidedIdeal.mem_unop_iff, isLinearTopology_iff_hasBasis_twoSidedIdeal, TwoSidedIdeal.inf_ringCon, MvPowerSeries.LinearTopology.hasBasis_nhds_zero, TwoSidedIdeal.subtype_apply, TwoSidedIdeal.matrix_strictMono_of_nonempty, TwoSidedIdeal.zero_mem, IsLinearTopology.hasBasis_open_twoSidedIdeal, TwoSidedIdeal.coe_asIdeal, TwoSidedIdeal.mem_mk', TwoSidedIdeal.mem_bot, TwoSidedIdeal.instAddSubgroupClass, TwoSidedIdeal.coe_mop_smul, TwoSidedIdeal.mem_sInf

---

← Back to Index