| Metric | Count |
|---|
DefinitionsAddOpposite, instAdd, instDecidableEq, instDiv, instInhabited, instInv, instInvolutiveInv, instInvolutiveNeg, instMul, instNeg, instOne, instUnique, instVAdd, instZero, op, opEquiv, rec', unop, instAdd, instDecidableEq, instInhabited, instInv, instInvolutiveInv, instInvolutiveNeg, instMul, instNeg, instOne, instSMul, instSub, instUnique, instZero, op, opEquiv, rec', unop, PreOpposite, unop', Β«term_α΅α΅α΅Β», Β«term_α΅α΅α΅Β» | 39 |
Theoremsexists, forall, instIsEmpty, instNontrivial, instSubsingleton, opEquiv_apply, opEquiv_symm_apply, op_add, op_bijective, op_comp_unop, op_div, op_eq_one_iff, op_eq_zero_iff, op_inj, op_injective, op_inv, op_mul, op_neg, op_one, op_surjective, op_unop, op_vadd, op_zero, unop_add, unop_bijective, unop_comp_op, unop_div, unop_eq_one_iff, unop_eq_zero_iff, unop_inj, unop_injective, unop_inv, unop_mul, unop_neg, unop_one, unop_op, unop_surjective, unop_vadd, unop_zero, exists, forall, instIsCancelAdd, instIsEmpty, instIsLeftCancelAdd, instIsRightCancelAdd, instNontrivial, instSubsingleton, isCancelAdd_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff, opEquiv_apply, opEquiv_symm_apply, op_add, op_bijective, op_comp_unop, op_eq_one_iff, op_eq_zero_iff, op_inj, op_injective, op_inv, op_mul, op_ne_zero_iff, op_neg, op_one, op_smul, op_sub, op_surjective, op_unop, op_zero, unop_add, unop_bijective, unop_comp_op, unop_eq_one_iff, unop_eq_zero_iff, unop_inj, unop_injective, unop_inv, unop_mul, unop_ne_zero_iff, unop_neg, unop_one, unop_op, unop_smul, unop_sub, unop_surjective, unop_zero | 86 |
| Total | 125 |
| Name | Category | Theorems |
|---|
instAdd π | CompOp | 113 mathmath: AddSubgroup.centerToAddOpposite_apply_coe, addCommute_op, AddSubsemigroup.op_iSup, HahnSeries.addOppositeEquiv_symm_support, UniqueAdd.iff_addOpposite, AddSubsemigroup.op_eq_top, AddSubsemigroup.unop_iInf, instContinuousAdd, AddSubsemigroup.le_op_iff, opAddEquiv_apply, AddSubsemigroup.op_le_iff, even_op_iff, AddUnits.coe_unop_opEquiv, AddHom.fromOpposite_apply, AddMonoidAlgebra.opRingEquiv_symm_single, AddMonoidAlgebra.opRingEquiv_symm_apply, AddSubsemigroup.unop_sSup, AddSubsemigroup.unop_iSup, isAddRightRegular_op, AddSubsemigroup.op_top, AddSubsemigroup.op_eq_bot, HahnSeries.addOppositeEquiv_support, AddSubmonoid.centerToAddOpposite_symm_apply_coe, AddSubsemigroup.mem_unop, AddSubsemigroup.centerToAddOpposite_symm_apply_coe, AddHom.op_apply_apply, AddSubsemigroup.unop_eq_bot, Finset.map_op_nsmul, AddSubsemigroup.op_iInf, unop_mem_center_iff, AddSubsemigroup.op_sInf, AddSubsemigroup.unop_sup, AddSubsemigroup.opEquiv_symm_apply, AddEquiv.op_symm_apply_symm_apply, AddEquiv.neg'_apply, DomAddAct.symm_mk_add, AddSubsemigroup.op_le_op_iff, even_unop_iff, Finset.map_op_add, AddHom.op_symm_apply_apply, AddSubsemigroup.op_sup, DomAddAct.mk_add, AddSubsemigroup.op_sSup, addSemiconjBy_unop, AddSubsemigroup.unop_sInf, isAddRightRegular_unop, instIsCancelAdd, AddCommute.op, op_sub, instMeasurableMulβ, HahnSeries.addOppositeEquiv_orderTop, coe_opAddEquiv, AddSubsemigroup.unop_injective, op_mem_center_iff, AddSubsemigroup.coe_unop, isAddLeftRegular_unop, AddSubsemigroup.unop_top, TwoUniqueSums.instAddOpposite, AddMonoidAlgebra.opRingEquiv_single, instIsLeftCancelAdd, isAddLeftRegular_op, coe_symm_opAddEquiv, AddSubsemigroup.op_injective, AddSubsemigroup.unop_bot, AddSubsemigroup.unop_inf, AddSubsemigroup.equivOp_symm_apply_coe, AddEquiv.opOp_symm_apply, AddMonoidAlgebra.opRingEquiv_apply, AddSubsemigroup.mem_op, AddHom.toOpposite_apply, HahnSeries.addOppositeEquiv_symm_orderTop, isAddRegular_unop, IsAddLeftRegular.op, AddSubsemigroup.unop_le_unop_iff, AddEquiv.opOp_apply, AddSubgroup.centerToAddOpposite_symm_apply_coe, opAddEquiv_symm_apply, op_add, AddCon.orderIsoOp_apply, addSemiconjBy_op, AddSubsemigroup.op_bot, HahnSeries.addOppositeEquiv_symm_leadingCoeff, HahnSeries.addOppositeEquiv_leadingCoeff, instMeasurableAdd, Set.image_op_add, IsAddRightRegular.op, Finset.image_op_add, AddSubsemigroup.op_closure, AddSemiconjBy.op, AddEquiv.neg'_symm_apply, AddSubsemigroup.opEquiv_apply, HahnSeries.addOppositeEquiv_symm_apply_coeff, AddSubsemigroup.equivOp_apply_coe, HahnSeries.addOppositeEquiv_apply, AddUnits.coe_opEquiv_symm, UniqueAdd.to_addOpposite, AddCon.orderIsoOp_symm_apply, AddSubsemigroup.centerToAddOpposite_apply_coe, AddEquiv.op_symm_apply_apply, AddSubsemigroup.op_inf, Finset.image_op_nsmul, instIsRightCancelAdd, IsAddRegular.op, UniqueSums.instAddOpposite, AddSubsemigroup.coe_op, AddSubsemigroup.unop_closure, AddEquiv.op_apply_symm_apply, isAddRegular_op, addCommute_unop, AddSubmonoid.centerToAddOpposite_apply_coe, unop_add, AddSubsemigroup.unop_eq_top, AddEquiv.op_apply_apply
|
instDecidableEq π | CompOp | 7 mathmath: Finset.map_op_nsmul, Finset.map_op_add, Finset.map_op_neg, Finset.image_op_zero, Finset.image_op_add, Finset.image_op_nsmul, Finset.image_op_neg
|
instDiv π | CompOp | 2 mathmath: op_div, unop_div
|
instInhabited π | CompOp | β |
instInv π | CompOp | 2 mathmath: op_inv, unop_inv
|
instInvolutiveInv π | CompOp | β |
instInvolutiveNeg π | CompOp | β |
instMul π | CompOp | 7 mathmath: opMulEquiv_symm_apply, unop_mul, opMulEquiv_toEquiv, instContinuousMulAddOpposite, opMulEquiv_apply, instNoZeroDivisors, op_mul
|
instNeg π | CompOp | 9 mathmath: DomAddAct.symm_mk_neg, Finset.map_op_neg, op_sub, op_neg, DomAddAct.mk_neg, instContinuousNegAddOpposite, unop_neg, Set.image_op_neg, Finset.image_op_neg
|
instOne π | CompOp | 8 mathmath: op_le_one, op_one, one_le_op, unop_eq_one_iff, one_le_unop, unop_le_one, unop_one, op_eq_one_iff
|
instUnique π | CompOp | β |
instVAdd π | CompOp | 13 mathmath: unop_vadd_eq_unop_vadd_unop, instVAddAssocClass, VAddAssocClass.opposite_mid, VAddAssocClass.op_right, continuousVAdd, instIsIsometricVAddAddOpposite, instIsCentralVAdd, op_vadd, unop_vadd, uniformContinuousConstVAdd, op_vadd_eq_op_vadd_op, instVAddCommClass, continuousConstVAdd
|
instZero π | CompOp | 24 mathmath: HahnSeries.addOppositeEquiv_symm_support, HahnSeries.addOppositeEquiv_support, Finset.map_op_nsmul, unop_eq_zero_iff, unop_nonpos, Finset.map_op_zero, Finset.image_op_zero, op_nonpos, nonneg_op, HahnSeries.addOppositeEquiv_orderTop, nonneg_unop, HahnSeries.addOppositeEquiv_symm_orderTop, unop_zero, HahnSeries.addOppositeEquiv_symm_leadingCoeff, HahnSeries.addOppositeEquiv_leadingCoeff, DomAddAct.mk_zero, op_eq_zero_iff, HahnSeries.addOppositeEquiv_symm_apply_coeff, HahnSeries.addOppositeEquiv_apply, instNoZeroDivisors, Set.image_op_zero, Finset.image_op_nsmul, DomAddAct.symm_mk_zero, op_zero
|
op π | CompOp | 150 mathmath: AddSubgroup.centerToAddOpposite_apply_coe, addCommute_op, measurable_add_op, comap_op_leftUniformSpace, rightAddCoset_zero, Finset.neg_op_vadd_finset_distrib, rightAddCoset_mem_rightAddCoset, UniqueAdd.iff_addOpposite, AddSubgroup.coe_unop, op_le_one, Finset.add_singleton, Set.op_vadd_set_add_eq_add_vadd_set, opAddEquiv_apply, even_op_iff, Finset.op_vadd_stabilizer_of_no_doubling, Set.op_vadd_set_subset_add, mem_rightAddCoset, isAddRightRegular_op, comap_uniformity_addOpposite, edist_op, AddSubgroup.unop_closure, Set.neg_op_vadd_set_distrib, op_injective, op_one, AddSubsemigroup.mem_unop, AddHom.op_apply_apply, nndist_op, op_vadd_add, opHomeomorph_apply, op_div, Finset.op_vadd_finset_subset_add, op_zsmul, AddSubmonoid.equivOp_apply_coe, one_le_op, op_unop, Set.image_op_vadd, exists, op_vadd, AddEquiv.op_symm_apply_symm_apply, AddEquiv.neg'_apply, IsCentralVAdd.op_vadd_eq_vadd, comap_unop_nhds, op_vadd_coe_set, continuous_op, Finset.add_subset_iff_right, op_vadd_op_vadd, AddHom.op_symm_apply_apply, uniformContinuous_op, mem_rightAddCoset_iff, Set.iUnion_op_vadd_set, AddMonoidHom.op_symm_apply_apply, Finset.biUnion_op_vadd_finset, opEquiv_apply, AddSubmonoid.unop_closure, op_bijective, Set.add_pair, op_comp_unop, Finset.image_op_zero, isAddUnit_op, comap_op_nhds, Finset.op_vadd_finset_add_eq_add_vadd_finset, AddCommute.op, op_nonpos, op_sub, AddMonoidHom.op_apply_apply, nonneg_op, AddSubmonoid.mem_unop, coe_opAddEquiv, rightAddCoset_eq_iff, op_mem_center_iff, AddSubsemigroup.coe_unop, op_neg, AddAction.op_vadd_set_stabilizer_subset, eq_addCosets_of_normal, AddSubmonoid.coe_unop, AddUnits.embedProduct_apply, op_le_op, AddMonoidAlgebra.opRingEquiv_single, isAddLeftRegular_op, Finset.op_vadd_addConvolution_eq_addConvolution_vadd, op_finsuppProd, op_eq_one_iff, AddHom.toOpposite_apply, IsAddLeftRegular.op, op_surjective, AddEquiv.opOp_apply, op_inv, op_add, op_nnratCast, leftAddCoset_rightAddCoset, op_natCast, op_vadd_eq_op_vadd_op, mem_own_rightAddCoset, addSemiconjBy_op, HahnSeries.addOppositeEquiv_symm_leadingCoeff, op_pow, op_intCast, unop_op, op_ratCast, forall, Set.add_subset_iff_right, Finset.addETransformLeft_fst, Set.image_op_add, Set.neg_vadd_set_distrib, op_vadd_eq_add, rightAddCoset_assoc, IsAddRightRegular.op, Finset.image_op_add, AddSemiconjBy.op, op_eq_zero_iff, unop_comp_op, op_ofNat, HahnSeries.addOppositeEquiv_symm_apply_coeff, dist_op, AddSubsemigroup.equivOp_apply_coe, Finset.op_prod, AddSubgroup.mem_unop, AddSubgroup.equivOp_apply_coe, orbit_addSubgroup_eq_rightCoset, normal_iff_eq_addCosets, HahnSeries.addOppositeEquiv_apply, AddUnits.coe_opEquiv_symm, op_inj, UniqueAdd.to_addOpposite, opMulEquiv_apply, Finset.addConvolution_op_vadd_eq_addConvolution_add_neg, op_nsmul, IsOpen.right_addCoset, AddSubsemigroup.centerToAddOpposite_apply_coe, Set.image_op_zero, Set.image_op_neg, AddEquiv.op_symm_apply_apply, IsClosed.right_addCoset, Finset.image_op_nsmul, Finset.addETransformRight_fst, IsAddRegular.op, AddSubsemigroup.unop_closure, comap_op_rightUniformSpace, op_zero, AddEquiv.op_apply_symm_apply, isAddRegular_op, Finset.image_op_neg, Finset.neg_vadd_finset_distrib, AddSubmonoid.centerToAddOpposite_apply_coe, Set.image_op_vadd_distrib, IsAddUnit.op, op_mul, AddMonoidHom.toOpposite_apply, AddEquiv.op_apply_apply, map_op_nhds
|
opEquiv π | CompOp | 9 mathmath: AddMonoidAlgebra.opRingEquiv_symm_apply, Finset.map_op_nsmul, Finset.map_op_add, Finset.map_op_zero, Finset.map_op_neg, opEquiv_apply, opMulEquiv_toEquiv, AddMonoidAlgebra.opRingEquiv_apply, opEquiv_symm_apply
|
rec' π | CompOp | β |
unop π | CompOp | 107 mathmath: AddCommute.unop, unop_vadd_eq_unop_vadd_unop, isAddUnit_unop, unop_intCast, IsAddLeftRegular.unop, HahnSeries.addOppositeEquiv_symm_support, unop_pow, opMulEquiv_symm_apply, AddUnits.coe_unop_opEquiv, AddHom.fromOpposite_apply, AddMonoidAlgebra.opRingEquiv_symm_single, HahnSeries.addOppositeEquiv_support, AddSubmonoid.centerToAddOpposite_symm_apply_coe, AddSubsemigroup.centerToAddOpposite_symm_apply_coe, AddHom.op_apply_apply, unop_mul, dist_unop, unop_nnratCast, IsCentralVAdd.unop_vadd_eq_vadd, AddMonoidHom.fromOpposite_apply, op_unop, unop_mem_center_iff, Finset.unop_prod, uniformContinuous_unop, Set.op_vadd_inter_ne_empty_iff, AddEquiv.op_symm_apply_symm_apply, unop_ratCast, edist_unop, comap_unop_nhds, unop_eq_zero_iff, even_unop_iff, unop_vadd, AddSubgroup.op_closure, AddHom.op_symm_apply_apply, AddSubmonoid.mem_op, unop_nonpos, continuous_unop, AddMonoidHom.op_symm_apply_apply, addSemiconjBy_unop, isAddRightRegular_unop, AddSubgroup.coe_op, op_comp_unop, AddSubgroup.mem_op, unop_natCast, IsAddUnit.unop, comap_op_nhds, unop_eq_one_iff, unop_ofNat, AddMonoidHom.op_apply_apply, HahnSeries.addOppositeEquiv_orderTop, unop_zsmul, one_le_unop, nonneg_unop, unop_le_one, isAddLeftRegular_unop, unop_one, unop_finsuppProd, coe_symm_opAddEquiv, Set.op_vadd_inter_nonempty_iff, AddSubsemigroup.equivOp_symm_apply_coe, AddEquiv.opOp_symm_apply, AddSubsemigroup.mem_op, opEquiv_symm_apply, HahnSeries.addOppositeEquiv_symm_orderTop, isAddRegular_unop, AddUnits.range_embedProduct, IsAddRegular.unop, AddSubgroup.centerToAddOpposite_symm_apply_coe, opAddEquiv_symm_apply, unop_zero, vadd_eq_add_unop, unop_le_unop, HahnSeries.addOppositeEquiv_symm_leadingCoeff, HahnSeries.addOppositeEquiv_leadingCoeff, unop_op, unop_inv, unop_nsmul, AddSubmonoid.op_closure, unop_sub, map_unop_nhds, AddSubsemigroup.op_closure, unop_comp_op, unop_surjective, unop_injective, AddEquiv.neg'_symm_apply, HahnSeries.addOppositeEquiv_symm_apply_coeff, IsAddRightRegular.unop, unop_div, AddSubmonoid.coe_op, HahnSeries.addOppositeEquiv_apply, measurable_add_unop, AddUnits.coe_opEquiv_symm, AddSemiconjBy.unop, nndist_unop, unop_bijective, unop_neg, AddEquiv.op_symm_apply_apply, unop_inj, AddSubsemigroup.coe_op, AddSubmonoid.equivOp_symm_apply_coe, opHomeomorph_symm_apply, AddEquiv.op_apply_symm_apply, addCommute_unop, uniformity_addOpposite, AddSubgroup.equivOp_symm_apply_coe, unop_add, AddEquiv.op_apply_apply
|
| Name | Category | Theorems |
|---|
instAdd π | CompOp | 88 mathmath: Language.reverseIso_apply, RingEquiv.toOpposite_symm_apply, RingEquiv.op_apply_apply, Polynomial.opRingEquiv_op_monomial, RingEquiv.toOpposite_apply, opAddEquiv_apply, Submodule.LinearDisjoint.op, MonoidAlgebra.opRingEquiv_single, Polynomial.leadingCoeff_opRingEquiv, RingEquiv.mopMatrix_symm_apply, RingEquiv.op_apply_symm_apply, coe_opLinearEquiv_symm_addEquiv, RingEquiv.mopMatrix_apply, RingCon.unop_iff, MonoidAlgebra.opRingEquiv_symm_apply, AddMonoidAlgebra.opRingEquiv_symm_single, AddMonoidAlgebra.opRingEquiv_symm_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, Subring.mopRingEquivOp_apply_coe, unop_add, RingEquiv.moduleEndSelf_symm_apply, Matrix.transposeRingEquiv_symm_apply, Polynomial.opRingEquiv_op_C, coe_opLinearEquiv_addEquiv, RingCon.op_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff, AddHom.mulOp_apply_apply, instIsCancelAdd, Subring.mopRingEquivOp_symm_apply, Polynomial.opRingEquiv_op_X, MonoidAlgebra.opRingEquiv_symm_single, RingInvo.involution', RingCon.opOrderIso_apply, RingEquiv.moduleEndSelf_apply, AddEquiv.mulOp_symm_apply, Submodule.equivOpposite_apply, AlgEquiv.toRingEquiv_unop, Matrix.transposeRingEquiv_apply, AddEquiv.mulOp_apply, instContinuousAddMulOpposite, AlgEquiv.toRingEquiv_opOp, AlgEquiv.op_symm_apply_symm_apply, Matrix.conjTransposeRingEquiv_symm_apply, Subsemiring.mopRingEquivOp_apply_coe, Polynomial.opRingEquiv_symm_C_mul_X_pow, Polynomial.opRingEquiv_symm_monomial, Submodule.linearDisjoint_op, Polynomial.support_opRingEquiv, AddMonoidAlgebra.opRingEquiv_single, RingCon.opOrderIso_symm_apply, op_add, AddHom.mulOp_symm_apply_apply, RingEquiv.op_symm_apply_symm_apply, AlgEquiv.toRingEquiv_op, AddMonoidAlgebra.opRingEquiv_apply, Subring.ringEquivOpMop_symm_apply_coe, opAddEquiv_toEquiv, RingInvo.coe_ringEquiv, Polynomial.coeff_opRingEquiv, Subsemiring.ringEquivOpMop_symm_apply_coe, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, RingEquiv.op_symm_apply_apply, AlgEquiv.opComm_symm_apply_symm_apply, AlgEquiv.toRingEquiv_toOpposite, Matrix.transposeAlgEquiv_symm_apply, Polynomial.opRingEquiv_symm_C, opLinearEquiv_symm_toAddEquiv, Subsemiring.ringEquivOpMop_apply, instIsRightCancelAdd, RingEquiv.unop_map_list_prod, Matrix.conjTransposeRingEquiv_apply, Language.reverseIso_symm_apply, Submodule.equivOpposite_symm_apply, Polynomial.natDegree_opRingEquiv, starRingEquiv_apply, Submodule.mulMap_op, Polynomial.opRingEquiv_op_C_mul_X_pow, RingEquiv.opOp_symm_apply, Subsemiring.mopRingEquivOp_symm_apply, Subring.ringEquivOpMop_apply, MonoidAlgebra.opRingEquiv_apply, RingEquiv.opOp_apply, opAddEquiv_symm_apply, instIsLeftCancelAdd, isCancelAdd_iff, Polynomial.opRingEquiv_symm_X, RingInvoClass.toRingEquivClass
|
instDecidableEq π | CompOp | 7 mathmath: Finset.image_op_inv, Finset.map_op_inv, Finset.image_op_one, Finset.image_op_mul, Finset.map_op_mul, Finset.image_op_pow, Finset.map_op_pow
|
instInhabited π | CompOp | β |
instInv π | CompOp | 10 mathmath: Finset.image_op_inv, MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, Finset.map_op_inv, Set.image_op_inv, DomMulAct.mk_inv, op_div, instContinuousInvMulOpposite, unop_inv, DomMulAct.symm_mk_inv, op_inv
|
instInvolutiveInv π | CompOp | β |
instInvolutiveNeg π | CompOp | β |
instMul π | CompOp | 192 mathmath: Language.reverseIso_apply, RingEquiv.toOpposite_symm_apply, TwoUniqueProds.instMulOpposite, RingEquiv.op_apply_apply, MulEquiv.inv'_apply, Polynomial.opRingEquiv_op_monomial, RingEquiv.toOpposite_apply, Subsemigroup.unop_iSup, Subsemigroup.centerToMulOpposite_apply_coe, MulHom.op_symm_apply_apply, Subsemigroup.op_le_op_iff, Submodule.LinearDisjoint.op, MonoidAlgebra.opRingEquiv_single, Polynomial.leadingCoeff_opRingEquiv, Subsemigroup.opEquiv_symm_apply, RingEquiv.mopMatrix_symm_apply, instIsRightCancelMulZeroOfIsLeftCancelMulZero, RingEquiv.op_apply_symm_apply, Subsemigroup.equivOp_symm_apply_coe, instContinuousMul, RingEquiv.mopMatrix_apply, RingCon.unop_iff, MonoidAlgebra.opRingEquiv_symm_apply, MulEquiv.opOp_symm_apply, AddMonoidAlgebra.opRingEquiv_symm_single, instIsCancelMulZero, AddMonoidAlgebra.opRingEquiv_symm_apply, MulEquiv.op_apply_symm_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, IsRightRegular.op, NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe, op_mem_center_iff, Subring.mopRingEquivOp_apply_coe, isCancelMulZero_iff, instMeasurableMulβ, RingEquiv.moduleEndSelf_symm_apply, Matrix.transposeRingEquiv_symm_apply, Polynomial.opRingEquiv_op_C, Submonoid.centerToMulOpposite_apply_coe, RingCon.op_iff, commute_unop, Subsemigroup.unop_eq_bot, instIsCancelMul, Subgroup.centerToMulOpposite_apply_coe, isRightCancelMulZero_iff, Subsemigroup.mem_op, UniqueMul.iff_mulOpposite, Subring.centerToMulOpposite_symm_apply_coe, coe_symm_opMulEquiv, Subsemigroup.op_iInf, Con.orderIsoOp_symm_apply, Subring.mopRingEquivOp_symm_apply, Polynomial.opRingEquiv_op_X, Subsemiring.centerToMulOpposite_symm_apply_coe, MonoidAlgebra.opRingEquiv_symm_single, unop_mul, RingInvo.involution', RingCon.opOrderIso_apply, RingEquiv.moduleEndSelf_apply, Subsemiring.centerToMulOpposite_apply_coe, Subsemigroup.unop_sup, Submodule.equivOpposite_apply, Subsemigroup.op_eq_top, Submonoid.centerToMulOpposite_symm_apply_coe, AlgEquiv.toRingEquiv_unop, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, Subsemigroup.coe_unop, Matrix.transposeRingEquiv_apply, isSquare_op_iff, opMulEquiv_apply, Units.coe_unop_opEquiv, MulEquiv.inv'_symm_apply, starMulEquiv_apply, Subsemigroup.unop_injective, MulEquiv.op_apply_apply, AlgEquiv.toRingEquiv_opOp, Subsemigroup.op_sup, Subring.centerToMulOpposite_apply_coe, AlgEquiv.op_symm_apply_symm_apply, Subsemigroup.unop_eq_top, Subsemigroup.centerToMulOpposite_symm_apply_coe, Finset.image_op_mul, isRegular_op, Matrix.conjTransposeRingEquiv_symm_apply, op_list_prod, Subsemiring.mopRingEquivOp_apply_coe, instIsRightCancelMul, Subsemigroup.op_iSup, Polynomial.opRingEquiv_symm_C_mul_X_pow, Subsemigroup.op_bot, Polynomial.opRingEquiv_symm_monomial, Submodule.linearDisjoint_op, Polynomial.support_opRingEquiv, AddMonoidAlgebra.opRingEquiv_single, RingCon.opOrderIso_symm_apply, isLeftRegular_op, Finset.map_op_mul, Subsemigroup.opEquiv_apply, Subsemigroup.op_closure, NonUnitalSubring.centerToMulOpposite_symm_apply_coe, RingEquiv.op_symm_apply_symm_apply, AlgEquiv.toRingEquiv_op, AddMonoidAlgebra.opRingEquiv_apply, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_Ο, commute_op, Con.orderIsoOp_apply, Subring.ringEquivOpMop_symm_apply_coe, Subsemigroup.op_sInf, RingInvo.coe_ringEquiv, Polynomial.coeff_opRingEquiv, Subsemiring.ringEquivOpMop_symm_apply_coe, unop_mem_center_iff, DomMulAct.stabilizerMulEquiv_apply, unop_list_prod, Subsemigroup.unop_sInf, op_div, isRightRegular_op, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, Subsemigroup.mem_unop, UniqueMul.to_mulOpposite, MulEquiv.opOp_apply, instMeasurableMul, op_mul, DomMulAct.mk_mul, UniqueProds.instMulOpposite, isSquare_unop_iff, RingEquiv.op_symm_apply_apply, MulHom.op_apply_apply, Subsemigroup.unop_bot, NonUnitalSubsemiring.centerToMulOpposite_apply_coe, instNoZeroDivisors, Units.coe_opEquiv_symm, instIsLeftCancelMulZeroOfIsRightCancelMulZero, AlgEquiv.opComm_symm_apply_symm_apply, AlgEquiv.toRingEquiv_toOpposite, Subsemigroup.unop_closure, Polynomial.opRingEquiv_symm_C, coe_opMulEquiv, MulEquiv.op_symm_apply_symm_apply, Subsemigroup.op_eq_bot, Subsemiring.ringEquivOpMop_apply, MulHom.toOpposite_apply, RingEquiv.unop_map_list_prod, DomMulAct.symm_mk_mul, Subsemigroup.unop_iInf, isRegular_unop, Finset.image_op_pow, Matrix.conjTransposeRingEquiv_apply, Language.reverseIso_symm_apply, SemiconjBy.op, IsRegular.op, Submodule.equivOpposite_symm_apply, Polynomial.natDegree_opRingEquiv, op_geom_sumβ, Subsemigroup.le_op_iff, starRingEquiv_apply, MulEquiv.op_symm_apply_apply, Submodule.mulMap_op, Subsemigroup.unop_le_unop_iff, Polynomial.opRingEquiv_op_C_mul_X_pow, Subsemigroup.coe_op, Subsemigroup.op_inf, RingEquiv.opOp_symm_apply, MulHom.fromOpposite_apply, Subsemiring.mopRingEquivOp_symm_apply, Subsemigroup.op_injective, Subsemigroup.equivOp_apply_coe, Commute.op, Subgroup.centerToMulOpposite_symm_apply_coe, Subsemigroup.unop_sSup, Subsemigroup.op_sSup, NonUnitalSubring.centerToMulOpposite_apply_coe, opMulEquiv_symm_apply, isRightRegular_unop, Subring.ringEquivOpMop_apply, Set.image_op_mul, Subsemigroup.unop_top, Subsemigroup.op_top, MonoidAlgebra.opRingEquiv_apply, IsLeftRegular.op, RingEquiv.opOp_apply, Finset.map_op_pow, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, semiconjBy_unop, Subsemigroup.unop_inf, isLeftRegular_unop, Polynomial.opRingEquiv_symm_X, RingInvoClass.toRingEquivClass, Subsemigroup.op_le_iff, semiconjBy_op, instIsLeftCancelMul, isLeftCancelMulZero_iff
|
instNeg π | CompOp | 4 mathmath: unop_neg, associator_op, instContinuousNegMulOpposite, op_neg
|
instOne π | CompOp | 18 mathmath: Finset.map_op_one, op_eq_one_iff, normOneClass, one_le_op, Finset.image_op_one, DomMulAct.symm_mk_one, one_le_unop, op_list_prod, unop_one, op_one, unop_list_prod, Set.image_op_one, Finset.image_op_pow, unop_eq_one_iff, unop_le_one, DomMulAct.mk_one, op_le_one, Finset.map_op_pow
|
instSMul π | CompOp | 18 mathmath: AlgEquiv.moduleEndSelfOp_apply_apply, continuousConstSMul, instIsScalarTower, IsScalarTower.opposite_mid, op_smul_eq_op_smul_op, uniformContinuousConstSMul, unop_smul, op_smul, IsScalarTower.op_right, instIsCentralScalar, AlgEquiv.moduleEndSelfOp_symm_apply, continuousSMul, instStarModule, instIsIsometricSMulMulOpposite, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, instFaithfulSMulMulOpposite_1, unop_smul_eq_unop_smul_unop, instSMulCommClass
|
instSub π | CompOp | 2 mathmath: unop_sub, op_sub
|
instUnique π | CompOp | β |
instZero π | CompOp | 40 mathmath: op_eq_zero_iff, ZeroAtInftyContinuousMap.instIsCentralScalar, instIsRightCancelMulZeroOfIsLeftCancelMulZero, BoundedContinuousFunction.instIsCentralScalar, Matrix.op_smul_one_eq_diagonal, instIsCancelMulZero, IsBoundedSMul.op, isCancelMulZero_iff, op_zero, isRightCancelMulZero_iff, Matrix.op_smul_eq_mul_diagonal, Matrix.mul_single_eq_updateCol_zero, Matrix.vecMul_ofNat, Finset.inv_smul_finset_distribβ, Set.inv_smul_set_distribβ, CompactlySupportedContinuousMap.instIsCentralScalar, op_nonpos, unop_zero, unop_nonpos, IsLeftCancelMulZero.toFaithfulSMul_opposite, Matrix.kronecker_ofNat, Matrix.mulVec_eq_sum, Finset.inv_op_smul_finset_distribβ, NonUnitalSeminormedRing.isBoundedSMulOpposite, Matrix.vecMul_diagonal_const, Matrix.vecMul_natCast, Matrix.trace_mul_single, instNoZeroDivisors, instIsLeftCancelMulZeroOfIsRightCancelMulZero, Matrix.vecMulVec_mulVec, op_nonneg, TwoSidedIdeal.instSMulMemClassMulOpposite, RingInvo.map_eq_zero_iff, Matrix.mulVec_single, Matrix.vecMul_intCast, Matrix.kronecker_diagonal, unop_nonneg, Set.inv_op_smul_set_distribβ, isLeftCancelMulZero_iff, unop_eq_zero_iff
|
op π | CompOp | 358 mathmath: DoubleCoset.doubleCoset_union_rightCoset, HasStrictFDerivAt.fun_mul', Subring.coe_unop, Language.reverseIso_apply, AlgEquiv.opOp_apply, op_eq_one_iff, Finset.mul_subset_iff_right, hasStrictFDerivAt_list_prod_finRange', TrivSqZeroExt.lift_inlAlgHom_inrHom, op_finsuppSum, op_eq_zero_iff, mem_own_rightCoset, op_ratCast, Finset.image_op_inv, RingEquiv.op_apply_apply, TrivSqZeroExt.snd_pow_eq_sum, MulEquiv.inv'_apply, Monoid.Foldl.ofFreeMonoid_apply, Polynomial.opRingEquiv_op_monomial, RingEquiv.toOpposite_apply, Subring.addEquivOp_apply_coe, AlgEquiv.toOpposite_apply, Finset.op_smul_finset_mul_eq_mul_smul_finset, fderivWithin_fun_pow', Subsemigroup.centerToMulOpposite_apply_coe, Finset.inv_smul_finset_distrib, Finset.doubling_lt_three_halves, MulHom.op_symm_apply_apply, opAddEquiv_apply, AlgEquiv.op_apply_apply, Submodule.LinearDisjoint.op, MonoidAlgebra.opRingEquiv_single, CliffordAlgebra.op_reverse, RootPairing.range_weylGroup_coweightHom, HasStrictFDerivAt.mul', Subgroup.unop_closure, Polynomial.leadingCoeff_opRingEquiv, op_injective, RingEquiv.mopMatrix_symm_apply, TrivSqZeroExt.snd_list_prod, Finset.op_smul_finset_subset_mul, measurable_mul_op, fderiv_fun_pow', RingEquiv.op_apply_symm_apply, op_star, one_le_op, map_op_nhds, op_smul_eq_op_smul_op, RingHom.toOpposite_apply, RingEquiv.mopMatrix_apply, RingCon.unop_iff, Finset.inv_op_smul_finset_distrib, rightCoset_eq_iff, MonoidAlgebra.opRingEquiv_symm_apply, op_unop, AlgHom.op_apply_apply, op_ofNat, Matrix.op_smul_one_eq_diagonal, AddMonoidAlgebra.opRingEquiv_symm_single, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Module.Basis.mulOpposite_apply, AddMonoidAlgebra.opRingEquiv_symm_apply, FormalMultilinearSeries.ofScalarsSum_op, MulEquiv.op_apply_symm_apply, Subsemiring.addEquivOp_apply_coe, IsRightRegular.op, HasStrictFDerivAt.list_prod', op_mem_center_iff, MulAction.op_smul_set_stabilizer_subset, Subring.mopRingEquivOp_apply_coe, edist_op, Finset.smul_inv_mul_eq_inv_mul_opSMul, algebraMap_apply, RingEquiv.moduleEndSelf_symm_apply, op_smul_eq_mul, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, Matrix.vecMulVec_update, op_zero, Polynomial.opRingEquiv_op_C, Subalgebra.mopAlgEquivOp_symm_apply, Submonoid.centerToMulOpposite_apply_coe, AlgHom.opComm_symm_apply_apply, Finset.image_op_one, Subsemiring.unop_closure, fderiv_mul_const', AddMonoidHom.mulOp_apply_apply, TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf, Subgroup.centerToMulOpposite_apply_coe, AlgEquiv.op_apply_symm_apply, AlgEquiv.mopMatrix_apply, isUnit_op, associator_op, TrivSqZeroExt.mul_left_eq_one, comap_unop_nhds, inner_op, fderiv_pow', forall, Algebra.TensorProduct.opAlgEquiv_apply, AddHom.mulOp_apply_apply, UniqueMul.iff_mulOpposite, op_smul_coe_set, op_pow, fderivWithin_fun_mul', hasFDerivAt_list_prod', Subalgebra.linearEquivOp_apply_coe, fderiv_mul', Module.Basis.mulOpposite_repr_op, op_smul, Matrix.op_smul_eq_mul_diagonal, Subring.mopRingEquivOp_symm_apply, Polynomial.opRingEquiv_op_X, NormedSpace.exp_op, nndist_op, MonoidAlgebra.opRingEquiv_symm_single, hasFDerivWithinAt_pow', exists, Matrix.mul_single_eq_updateCol_zero, fderivWithin_mul_const', Subsemiring.centerToMulOpposite_apply_coe, hasFDerivAt_list_prod_finRange', Submodule.equivOpposite_apply, mem_rightCoset, normal_iff_eq_cosets, TrivSqZeroExt.snd_inv, NonUnitalRingHom.toOpposite_apply, op_smul_op_smul, Subsemigroup.coe_unop, Matrix.transposeRingEquiv_apply, coe_opLinearEquiv_toLinearMap, op_natCast, Set.op_smul_set_mul_eq_mul_smul_set, isSquare_op_iff, Matrix.vecMul_ofNat, opMulEquiv_apply, Finset.inv_smul_finset_distribβ, opEquiv_apply, HasFDerivWithinAt.mul_const', nnnorm_op, starMulEquiv_apply, MonoidHom.op_symm_apply_apply, Subring.mem_unop, fderiv_pow_ring', MulEquiv.op_apply_apply, Set.inv_smul_set_distribβ, HasSum.op, Subring.centerToMulOpposite_apply_coe, op_le_op, dist_op, AlgEquiv.op_symm_apply_symm_apply, hasSum_op, Matrix.map_op_smul', HasFDerivAt.fun_pow', HasMFDerivWithinAt.mul', Monoid.foldlM.ofFreeMonoid_apply, TrivSqZeroExt.inr_mul_inl, Finset.image_op_mul, TrivSqZeroExt.snd_invOf, QuaternionAlgebra.coe_starAe, isRegular_op, Subalgebra.mem_unop, op_nonpos, uniformContinuous_op, op_list_prod, op_neg, Subsemiring.mopRingEquivOp_apply_coe, Subalgebra.unop_adjoin, hasStrictFDerivAt_pow', RingHom.op_symm_apply_apply, Polynomial.opRingEquiv_symm_C_mul_X_pow, fderiv_fun_mul', Set.inv_smul_set_distrib, Polynomial.opRingEquiv_symm_monomial, Submodule.linearDisjoint_op, IsOpen.rightCoset, Matrix.vecMulVec_smul', Matrix.kronecker_ofNat, Matrix.mulVec_eq_sum, Submonoid.equivOp_apply_coe, rightCoset_mem_rightCoset, Finset.inv_op_smul_finset_distribβ, hasStrictFDerivAt_list_prod_attach', Matrix.scalar_comm_iff, AddMonoidAlgebra.opRingEquiv_single, isLeftRegular_op, Subalgebra.algEquivOpMop_apply, Set.iUnion_op_smul_set, TrivSqZeroExt.snd_mul, Matrix.vecMul_diagonal_const, op_add, AddHom.mulOp_symm_apply_apply, Set.mul_pair, RingEquiv.op_symm_apply_symm_apply, AddMonoidAlgebra.opRingEquiv_apply, commute_op, op_inj, Subgroup.coe_unop, Finset.op_smul_convolution_eq_convolution_smul, Subgroup.equivOp_apply_coe, Set.image_op_inv, HasFDerivWithinAt.pow', HasFDerivAt.list_prod', hasFDerivAt_pow', Set.mul_subset_iff_right, Subring.unop_closure, Matrix.vecMul_natCast, Polynomial.coeff_opRingEquiv, comap_uniformity_mulOpposite, Quaternion.coe_starAe, norm_op, isRightRegular_iff, comap_op_leftUniformSpace, op_one, Set.image_op_smul, Matrix.trace_mul_single, op_div, isRightRegular_op, Subsemigroup.mem_unop, unop_op, Finset.mulETransformRight_fst, UniqueMul.to_mulOpposite, orbit_subgroup_eq_rightCoset, op_geom_sum, MulEquiv.opOp_apply, CliffordAlgebra.reverseOp_ΞΉ, Matrix.transposeAlgEquiv_apply, op_mul, comap_op_nhds, Set.inv_op_smul_set_distrib, Set.op_smul_set_subset_mul, RingEquiv.op_symm_apply_apply, HasFDerivAt.pow', HasStrictFDerivAt.pow', MulHom.op_apply_apply, NonUnitalSubsemiring.centerToMulOpposite_apply_coe, Subalgebra.coe_unop, HasStrictFDerivAt.mul_const', Set.image_op_one, AlgEquiv.opComm_symm_apply_apply, AlgEquiv.moduleEndSelf_symm_apply, Units.coe_opEquiv_symm, opLinearIsometryEquiv_apply, AlgEquiv.opComm_symm_apply_symm_apply, fderivWithin_list_prod', HasFDerivWithinAt.fun_mul', Set.image_op_smul_distrib, fderivWithin_pow_ring', Algebra.TensorProduct.opAlgEquiv_tmul, op_bijective, AlgEquiv.mopMatrix_symm_apply, eq_cosets_of_normal, TwoSidedIdeal.subtypeMop_apply, coe_opLinearEquiv, HasFDerivWithinAt.fun_pow', Subsemigroup.unop_closure, Polynomial.opRingEquiv_symm_C, Submonoid.mem_unop, coe_opMulEquiv, Matrix.vecMulVec_mulVec, HasFDerivAt.mul_const', summable_op, HasStrictFDerivAt.fun_pow', MulEquiv.op_symm_apply_symm_apply, Subsemiring.ringEquivOpMop_apply, AlgEquiv.op_symm_apply_apply, Finset.op_smul_stabilizer_of_no_doubling, MonoidHom.op_apply_apply, MulHom.toOpposite_apply, DualNumber.lift_op_smul, TrivSqZeroExt.mul_right_eq_one, opContinuousLinearEquiv_apply, op_nonneg, TwoSidedIdeal.coe_unop, op_zpow, AddMonoidHom.mulOp_symm_apply_apply, Finset.image_op_pow, Matrix.conjTransposeRingEquiv_apply, SemiconjBy.op, IsRegular.op, comap_op_rightUniformSpace, op_surjective, op_geom_sumβ, op_intCast, starRingEquiv_apply, MulEquiv.op_symm_apply_apply, Submodule.mulMap_op, Matrix.mulVec_single, hasStrictFDerivAt_list_prod', Rack.op_act_op_eq, IsUnit.op, Finset.biUnion_op_smul_finset, Polynomial.opRingEquiv_op_C_mul_X_pow, IsRightRegular.isSMulRegular, rightCoset_one, RingHom.op_apply_apply, Subsemiring.mopRingEquivOp_symm_apply, HasFDerivWithinAt.mul', Subsemigroup.equivOp_apply_coe, Submonoid.unop_closure, Commute.op, AlgHom.toOpposite_apply, leftCoset_rightCoset, Matrix.conjTranspose_smul_self, fderivWithin_mul', unop_comp_op, Matrix.vecMul_intCast, Subgroup.mem_unop, continuous_op, op_nnratCast, mem_rightCoset_iff, TwoSidedIdeal.mem_unop_iff, Submonoid.coe_unop, Matrix.scalar_commute_iff, Algebra.TensorProduct.opAlgEquiv_symm_tmul, tsum_op, Subalgebra.mopAlgEquivOp_apply_coe, fderiv_list_prod', HasMFDerivAt.mul', NonUnitalSubring.centerToMulOpposite_apply_coe, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, AlgHom.op_symm_apply_apply, Subring.ringEquivOpMop_apply, op_le_one, Set.image_op_mul, MonoidHom.toOpposite_apply, RootPairing.Equiv.coweightHom_apply, HasFDerivAt.fun_mul', MonoidAlgebra.opRingEquiv_apply, IsLeftRegular.op, RingEquiv.opOp_apply, op_comp_unop, Subsemiring.mem_unop, HasFDerivAt.mul', rightCoset_assoc, Finset.op_sum, hasFDerivAt_list_prod_attach', Subgroup.smul_diff', Finset.mulETransformLeft_fst, op_inv, TrivSqZeroExt.mul_inl_eq_op_smul, IsCentralScalar.op_smul_eq_smul, Matrix.kronecker_diagonal, Finset.mul_singleton, op_smul_mul, Polynomial.opRingEquiv_symm_X, Subsemiring.coe_unop, Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves, Set.inv_op_smul_set_distribβ, Units.embedProduct_apply, op_sub, semiconjBy_op, opHomeomorph_apply, IsClosed.rightCoset, Rack.op_invAct_op_eq, HasFDerivWithinAt.list_prod', Matrix.col_vecMulVec, Finset.convolution_op_smul_eq_convolution_mul_inv, fderivWithin_pow', Summable.op
|
opEquiv π | CompOp | 9 mathmath: Finset.map_op_one, Finset.map_op_inv, MonoidAlgebra.opRingEquiv_symm_apply, opEquiv_apply, opEquiv_symm_apply, Finset.map_op_mul, opAddEquiv_toEquiv, MonoidAlgebra.opRingEquiv_apply, Finset.map_op_pow
|
rec' π | CompOp | β |
unop π | CompOp | 210 mathmath: CliffordAlgebra.unop_reverseOp, unop_zpow, RingEquiv.toOpposite_symm_apply, Submonoid.equivOp_symm_apply_coe, Subalgebra.mem_op, RingEquiv.op_apply_apply, SemiconjBy.unop, Subgroup.equivOp_symm_apply_coe, coe_opLinearEquiv_symm, Subring.coe_op, AlgEquiv.toOpposite_symm_apply, MulHom.op_symm_apply_apply, AlgEquiv.op_apply_apply, nnnorm_unop, unop_sub, Polynomial.leadingCoeff_opRingEquiv, RingEquiv.mopMatrix_symm_apply, RingEquiv.op_apply_symm_apply, IsCentralScalar.unop_smul_eq_smul, norm_unop, Set.op_smul_inter_ne_empty_iff, Subsemigroup.equivOp_symm_apply_coe, RingEquiv.mopMatrix_apply, MonoidAlgebra.opRingEquiv_symm_apply, op_unop, AlgHom.op_apply_apply, Monoid.CoprodI.inv_def, Subgroup.mem_op, MulEquiv.opOp_symm_apply, AddMonoidAlgebra.opRingEquiv_symm_single, AddMonoidAlgebra.opRingEquiv_symm_apply, MulEquiv.op_apply_symm_apply, NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe, Subring.mopRingEquivOp_apply_coe, CategoryTheory.End.smul_left, TwoSidedIdeal.mem_op_iff, unop_add, Matrix.transposeRingEquiv_symm_apply, unop_ofNat, unop_map_list_prod, NonUnitalRingHom.fromOpposite_apply, summable_unop, Subalgebra.op_adjoin, RingCon.op_iff, commute_unop, AddMonoidHom.mulOp_apply_apply, Subgroup.smul_diff_smul', AlgEquiv.op_apply_symm_apply, unop_neg, AlgEquiv.mopMatrix_apply, associator_op, Subalgebra.coe_op, comap_unop_nhds, Subsemiring.op_closure, edist_unop, unop_nnratCast, IsLeftRegular.unop, Subsemigroup.mem_op, AddHom.mulOp_apply_apply, unop_ratCast, AlgHom.opComm_apply_apply, unop_star, unop_smul, Subring.centerToMulOpposite_symm_apply_coe, AlgHom.mulLeftRight_apply, coe_symm_opMulEquiv, HasSum.unop, AlgEquiv.opComm_apply_apply, opContinuousLinearEquiv_symm_apply, Subsemiring.mem_op, Subsemiring.centerToMulOpposite_symm_apply_coe, unop_pow, MonoidAlgebra.opRingEquiv_symm_single, hasSum_unop, unop_mul, Subsemiring.addEquivOp_symm_apply_coe, RingInvo.involution', Submonoid.coe_op, continuous_unop, Submonoid.centerToMulOpposite_symm_apply_coe, TwoSidedIdeal.mem_asIdealOpposite, dist_unop, Set.op_smul_inter_nonempty_iff, Units.coe_unop_opEquiv, opEquiv_symm_apply, MulEquiv.inv'_symm_apply, MonoidHom.op_symm_apply_apply, Traversable.foldl.unop_ofFreeMonoid, MulEquiv.op_apply_apply, Subring.mem_op, inner_unop, AlgEquiv.op_symm_apply_symm_apply, Subsemigroup.centerToMulOpposite_symm_apply_coe, isUnit_unop, AlgHom.fromOpposite_apply, Summable.unop, one_le_unop, Matrix.conjTransposeRingEquiv_symm_apply, unop_le_unop, unop_zero, RingInvo.involution, unop_nonpos, Subsemiring.mopRingEquivOp_apply_coe, Algebra.TensorProduct.opAlgEquiv_symm_apply, RingHom.op_symm_apply_apply, Polynomial.opRingEquiv_symm_C_mul_X_pow, Polynomial.opRingEquiv_symm_monomial, opLinearIsometryEquiv_symm_apply, Polynomial.support_opRingEquiv, tsum_unop, Subsemigroup.op_closure, AddHom.mulOp_symm_apply_apply, RootPairing.Equiv.coweightHom_op, NonUnitalSubring.centerToMulOpposite_symm_apply_coe, RingEquiv.op_symm_apply_symm_apply, AddMonoidAlgebra.opRingEquiv_apply, unop_one, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_Ο, IsRegular.unop, unop_intCast, Subring.ringEquivOpMop_symm_apply_coe, Polynomial.coeff_opRingEquiv, Subsemiring.ringEquivOpMop_symm_apply_coe, AlgEquiv.moduleEndSelf_apply_apply, unop_mem_center_iff, DomMulAct.stabilizerMulEquiv_apply, unop_list_prod, unop_op, map_unop_nhds, opHomeomorph_symm_apply, comap_op_nhds, Submonoid.op_closure, isSquare_unop_iff, RingEquiv.op_symm_apply_apply, MulHom.op_apply_apply, unop_inj, Units.coe_opEquiv_symm, Subsemiring.coe_op, Subgroup.op_closure, AlgEquiv.opComm_symm_apply_symm_apply, Submonoid.mem_op, Algebra.TensorProduct.opAlgEquiv_tmul, unop_bijective, AlgEquiv.mopMatrix_symm_apply, Subalgebra.linearEquivOp_symm_apply_coe, unop_injective, unop_surjective, Polynomial.opRingEquiv_symm_C, IsRightRegular.unop, Subring.op_closure, unop_inv, MulEquiv.op_symm_apply_symm_apply, AlgEquiv.op_symm_apply_apply, MonoidHom.op_apply_apply, RingEquiv.unop_map_list_prod, RingHom.fromOpposite_apply, isRegular_unop, AddMonoidHom.mulOp_symm_apply_apply, CategoryTheory.Mat.equivalenceSingleObjInverse_map, Language.reverseIso_symm_apply, unop_eq_one_iff, smul_eq_mul_unop, Subgroup.coe_op, Submodule.equivOpposite_symm_apply, Polynomial.natDegree_opRingEquiv, TwoSidedIdeal.coe_op, MulEquiv.op_symm_apply_apply, unop_le_one, Subsemigroup.coe_op, coe_opLinearEquiv_symm_toLinearMap, RingEquiv.opOp_symm_apply, MulHom.fromOpposite_apply, RingHom.op_apply_apply, Commute.unop, RingInvoClass.involution, unop_comp_op, Subgroup.centerToMulOpposite_symm_apply_coe, Finset.unop_sum, nndist_unop, Subalgebra.mopAlgEquivOp_apply_coe, unop_natCast, Subalgebra.algEquivOpMop_symm_apply_coe, AlgHom.op_symm_apply_apply, opMulEquiv_symm_apply, RootPairing.Equiv.coweightHom_toLinearMap, isRightRegular_unop, Units.range_embedProduct, AlgEquiv.opOp_symm_apply, MonoidAlgebra.opRingEquiv_apply, opAddEquiv_symm_apply, op_comp_unop, unop_finsuppSum, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, Matrix.op_smul_eq_vecMul, unop_div, semiconjBy_unop, IsUnit.unop, isLeftRegular_unop, Module.Basis.repr_unop_eq_mulOpposite_repr, NormedSpace.exp_unop, uniformContinuous_unop, unop_nonneg, measurable_mul_unop, Subring.addEquivOp_symm_apply_coe, FormalMultilinearSeries.ofScalarsSum_unop, unop_eq_zero_iff, uniformity_mulOpposite, TwoSidedIdeal.coe_mop_smul, MonoidHom.fromOpposite_apply, unop_smul_eq_unop_smul_unop
|
| Name | Category | Theorems |
|---|
AddOpposite π | CompOp | 436 mathmath: AddSubgroup.centerToAddOpposite_apply_coe, AddOpposite.addCommute_op, measurable_add_op, AddOpposite.comap_op_leftUniformSpace, AddAction.stabilizer_addSubgroup_op, AddSubgroup.vadd_opposite_image_add_preimage', AddSubgroup.normal_op, AddSubsemigroup.op_iSup, Finset.isCentralVAdd, AddOpposite.unop_vadd_eq_unop_vadd_unop, rightAddCoset_zero, isAddUnit_unop, AddUnits.embedProduct_injective, AddOpposite.instT2Space, AddOpposite.unop_intCast, Finset.neg_op_vadd_finset_distrib, HahnSeries.addOppositeEquiv_symm_support, AddSubmonoid.unop_le_unop_iff, rightAddCoset_mem_rightAddCoset, AddSubmonoid.unop_inf, UniqueAdd.iff_addOpposite, AddSubmonoid.op_sup, AddSubgroup.op_inf, AddSubsemigroup.op_eq_top, AddOpposite.instVAddAssocClass, AddSubsemigroup.unop_iInf, Prod.isIsometricVAdd'', AddOpposite.instIsOrderedRing, AddSubgroup.coe_unop, UniformContinuousConstVAdd.op, AddOpposite.op_le_one, AddOpposite.unop_pow, AddOpposite.opMulEquiv_symm_apply, AddOpposite.instContinuousAdd, Finset.add_singleton, Set.op_vadd_set_add_eq_add_vadd_set, AddSubsemigroup.le_op_iff, AddOpposite.opAddEquiv_apply, VAddAssocClass.opposite_mid, AddSubsemigroup.op_le_iff, even_op_iff, AddUnits.coe_unop_opEquiv, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp, Finset.op_vadd_stabilizer_of_no_doubling, AddHom.fromOpposite_apply, Set.op_vadd_set_subset_add, AddMonoidAlgebra.opRingEquiv_symm_single, AddMonoidAlgebra.opRingEquiv_symm_apply, AddSubgroup.unop_normalizer, AddSubsemigroup.unop_sSup, AddSubgroup.unop_sInf, mem_rightAddCoset, AddSubgroup.op_le_iff, AddSubmonoid.unop_eq_bot, instFaithfulVAddAddOpposite, AddSubsemigroup.unop_iSup, isAddRightRegular_op, comap_uniformity_addOpposite, CompleteSpace.addOpposite, AddOpposite.edist_op, AddSubsemigroup.op_top, AddSubgroup.unop_closure, AddSubgroup.op_sInf, Set.neg_op_vadd_set_distrib, AddSubgroup.op_normalizer, VAddAssocClass.op_right, AddSubmonoid.unop_iInf, AddSubsemigroup.op_eq_bot, AddOpposite.op_injective, HahnSeries.addOppositeEquiv_support, AddSubmonoid.centerToAddOpposite_symm_apply_coe, AddOpposite.op_one, AddSubsemigroup.mem_unop, AddSubsemigroup.centerToAddOpposite_symm_apply_coe, AddSubmonoid.op_eq_top, AddHom.op_apply_apply, AddSubgroup.unop_inf, AddSubsemigroup.unop_eq_bot, instIsTopologicalRingAddOpposite, AddOpposite.nndist_op, AddSubmonoid.unop_bot, AddOpposite.unop_mul, AddOpposite.dist_unop, Cardinal.mk_addOpposite, op_vadd_add, AddOpposite.opHomeomorph_apply, Finset.map_op_nsmul, AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, AddAction.stabilizer_op_addSubgroup, AddOpposite.op_div, AddOpposite.continuousVAdd, Finset.op_vadd_finset_subset_add, AddOpposite.op_zsmul, AddSubmonoid.equivOp_apply_coe, AddSubmonoid.op_eq_bot, AddOpposite.one_le_op, AddOpposite.unop_nnratCast, IsCentralVAdd.unop_vadd_eq_vadd, instErgodicVAddAddOppositeOfIsAddRightInvariant, AddMonoidHom.fromOpposite_apply, instIsIsometricVAddAddOpposite, AddSubgroup.op.instNormal, PUnit.instIsCentralVAdd, AddOpposite.instIsCentralVAdd, Pi.isCentralVAdd, AddSubsemigroup.op_iInf, AddSubmonoid.unop_top, AddOpposite.unop_mem_center_iff, AddSubgroup.le_op_iff, AddSubgroup.unop_iSup, Finset.unop_prod, AddOpposite.uniformContinuous_unop, Set.image_op_vadd, AddSubgroup.op_top, AddSubsemigroup.op_sInf, AddSubgroup.op_toAddSubmonoid, AddSubsemigroup.unop_sup, AddSemigroup.opposite_vaddCommClass', AddSubsemigroup.opEquiv_symm_apply, AddOpposite.op_vadd, AddEquiv.op_symm_apply_symm_apply, AddSubgroup.op_le_op_iff, AddOpposite.unop_ratCast, AddEquiv.neg'_apply, AddOpposite.edist_unop, AddSubgroup.op_bot, IsCentralVAdd.op_vadd_eq_vadd, MeasurableVAdd.op, AddSubgroup.unop_injective, AddOpposite.comap_unop_nhds, AddSubgroup.op_toSubsemigroup, MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op, AddSubsemigroup.op_le_op_iff, AddSubgroup.vadd_opposite_add, op_vadd_coe_set, AddSubgroup.op_sup, AddOpposite.unop_eq_zero_iff, even_unop_iff, AddOpposite.continuous_op, SeparationQuotient.instIsCentralVAdd, Finset.add_subset_iff_right, AddOpposite.unop_vadd, op_vadd_op_vadd, Finset.map_op_add, AddSubgroup.op_closure, AddHom.op_symm_apply_apply, AddOpposite.instAddTorsionFree, AddOpposite.uniformContinuous_op, AddSubsemigroup.op_sup, AddSubmonoid.unop_iSup, AddOpposite.isDedekindFiniteAddMonoid_iff, AddSubmonoid.mem_op, VAddAssocClass.op_left, AddSubgroup.unop_toSubsemigroup, IsIsometricVAdd.opposite_of_comm, mem_rightAddCoset_iff, QuotientAddGroup.sound, AddOpposite.unop_nonpos, Set.iUnion_op_vadd_set, AddOpposite.continuous_unop, AddSubmonoid.unop_sInf, AddSubmonoid.op_top, AddSubsemigroup.op_sSup, AddMonoidHom.op_symm_apply_apply, Finset.biUnion_op_vadd_finset, Finset.map_op_zero, AddSubgroup.unop_sup, AddOpposite.addSemiconjBy_unop, AddOpposite.instIsDomain, Finset.map_op_neg, AddSubsemigroup.unop_sInf, AddOpposite.opEquiv_apply, Filter.isCentralVAdd, isAddRightRegular_unop, NormedAddGroup.to_isIsometricVAdd_right, AddSubgroup.coe_op, AddSubmonoid.unop_closure, AddOpposite.op_bijective, AddOpposite.instSubsingleton, Set.add_pair, AddOpposite.op_comp_unop, Finset.image_op_zero, ContinuousConstVAdd.op, AddSubmonoid.op_le_op_iff, AddSubgroup.mem_op, isAddUnit_op, AddOpposite.unop_natCast, AddOpposite.instIsCancelAdd, AddOpposite.comap_op_nhds, Finset.op_vadd_finset_add_eq_add_vadd_finset, AddSubmonoid.unop_sSup, AddSubgroup.isAddQuotientCoveringMap, AddOpposite.unop_eq_one_iff, AddCommute.op, AddSubgroup.opEquiv_symm_apply, AddOpposite.op_nonpos, AddOpposite.op_sub, SubAddAction.isCentralVAdd, AddMonoidHom.op_apply_apply, AddOpposite.nonneg_op, AddOpposite.instMeasurableMulβ, AddSubmonoid.op_inf, AddSubmonoid.mem_unop, AddOpposite.opMulEquiv_toEquiv, HahnSeries.addOppositeEquiv_orderTop, AddOpposite.instIsOrderedAddMonoid, AddSubgroup.op_sSup, AddOpposite.coe_opAddEquiv, rightAddCoset_eq_iff, AddSubsemigroup.unop_injective, instProperVAddAddOppositeOfIsTopologicalAddGroup, AddSubgroup.unop_eq_top, AddSubgroup.Normal.op, AddOpposite.op_mem_center_iff, AddSubsemigroup.coe_unop, AddSubgroup.unop_eq_bot, instIsTopologicalAddGroupAddOpposite, AddOpposite.op_neg, AddAction.op_vadd_set_stabilizer_subset, AddOpposite.unop_zsmul, AddOpposite.one_le_unop, AddOpposite.nonneg_unop, eq_addCosets_of_normal, AddOpposite.unop_le_one, AddOpposite.uniformContinuousConstVAdd, AddSubmonoid.coe_unop, isAddLeftRegular_unop, AddSubgroup.unop_bot, AddSubmonoid.op_sSup, AddUnits.embedProduct_apply, AddOpposite.unop_one, AddSubsemigroup.unop_top, AddOpposite.unop_finsuppProd, TwoUniqueSums.instAddOpposite, AddOpposite.op_le_op, AddOpposite.instNontrivial, AddMonoidAlgebra.opRingEquiv_single, AddSubmonoid.op_iSup, AddOpposite.instIsLeftCancelAdd, isAddLeftRegular_op, AddSubgroup.op_iInf, AddOpposite.coe_symm_opAddEquiv, Set.op_vadd_inter_nonempty_iff, AddSubsemigroup.op_injective, AddSubsemigroup.unop_bot, AddOpposite.instCompactSpace, Finset.op_vadd_addConvolution_eq_addConvolution_vadd, instContinuousMulAddOpposite, AddOpposite.op_finsuppProd, AddSubgroup.unop_iInf, UniformSpace.Completion.instIsCentralVAdd, AddSubsemigroup.unop_inf, AddSubsemigroup.equivOp_symm_apply_coe, AddEquiv.opOp_symm_apply, AddOpposite.instIsUniformAddGroup, Option.instIsCentralVAdd, AddOpposite.exponent, AddMonoidAlgebra.opRingEquiv_apply, AddOpposite.op_eq_one_iff, AddSubsemigroup.mem_op, AddOpposite.opEquiv_symm_apply, AddHom.toOpposite_apply, HahnSeries.addOppositeEquiv_symm_orderTop, AddSubmonoid.op_sInf, Sigma.instIsCentralVAdd, AddSubgroup.opEquiv_apply, isAddRegular_unop, ContinuousAdd.to_continuousVAdd_op, IsAddLeftRegular.op, AddOpposite.op_surjective, AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite, AddUnits.range_embedProduct, AddSubsemigroup.unop_le_unop_iff, AddEquiv.opOp_apply, AddSubgroup.op_injective, AddOpposite.op_inv, AddOreLocalization.instIsCentralVAdd, AddOpposite.instWeaklyLocallyCompactSpace, AddSubgroup.centerToAddOpposite_symm_apply_coe, ContinuousVAdd.op, AddOpposite.opAddEquiv_symm_apply, AddSubmonoid.op_le_iff, AddOpposite.op_add, AddCon.orderIsoOp_apply, AddOpposite.op_nnratCast, leftAddCoset_rightAddCoset, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, QuotientAddGroup.orbit_eq_out_vadd, AddSubmonoid.unop_injective, AddOpposite.op_natCast, AddOpposite.unop_zero, VAddCommClass.opposite_mid, AddOpposite.vadd_eq_add_unop, AddOpposite.op_vadd_eq_op_vadd_op, AddOpposite.unop_le_unop, AddSubmonoid.unop_eq_top, mem_own_rightAddCoset, AddOpposite.addSemiconjBy_op, AddSubgroup.Normal.of_unop, AddSubsemigroup.op_bot, instIsTopologicalSemiringAddOpposite, AddSemigroup.opposite_vaddCommClass, HahnSeries.addOppositeEquiv_symm_leadingCoeff, HahnSeries.addOppositeEquiv_leadingCoeff, AddAction.right_quotientAction, AddOpposite.op_pow, AddOpposite.op_intCast, instContinuousNegAddOpposite, AddOpposite.instMeasurableConstVAdd, AddOpposite.unop_inv, AddOpposite.unop_nsmul, AddOpposite.instMeasurableAdd, AddOpposite.op_ratCast, Prod.isCentralVAdd, AddSubmonoid.op_closure, Set.add_subset_iff_right, AddSubgroup.op_iSup, Finset.addETransformLeft_fst, AddOpposite.unop_sub, AddOpposite.map_unop_nhds, Set.image_op_add, Set.neg_vadd_set_distrib, op_vadd_eq_add, rightAddCoset_assoc, IsAddRightRegular.op, AddOpposite.instIsEmpty, Finset.image_op_add, AddSubsemigroup.op_closure, AddSemiconjBy.op, AddOpposite.op_eq_zero_iff, AddOpposite.unop_comp_op, AddOpposite.unop_surjective, Additive.isIsIsometricVAdd'', AddOpposite.unop_injective, AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, AddEquiv.neg'_symm_apply, AddSubsemigroup.opEquiv_apply, AddSubgroup.unop_toAddSubmonoid, HahnSeries.addOppositeEquiv_symm_apply_coeff, AddSubmonoid.unop_toSubsemigroup, AddSubgroup.unop_top, AddOpposite.instDiscreteTopology, AddSubmonoid.op_injective, AddOpposite.dist_op, Sum.instIsCentralVAdd, AddOpposite.unop_div, AddSubsemigroup.equivOp_apply_coe, Finset.op_prod, AddSubgroup.mem_unop, AddSubgroup.equivOp_apply_coe, orbit_addSubgroup_eq_rightCoset, VAddCommClass.op_right, AddSubgroup.op_eq_bot, AddSubmonoid.coe_op, normal_iff_eq_addCosets, AddSubgroup.unop_sSup, measurableVAdd_opposite_of_add, HahnSeries.addOppositeEquiv_apply, AddOpposite.instIsDedekindFiniteAddMonoid, measurable_add_unop, AddSubmonoid.op_iInf, Equiv.isCentralVAdd, AddSubgroup.vadd_opposite_image_add_preimage, AddOpposite.lipschitzAdd, AddSubgroup.normal_unop, AddUnits.coe_opEquiv_symm, AddOpposite.nndist_unop, instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe, instFaithfulVAddAddOppositeOfIsLeftCancelAdd, AddOpposite.unop_bijective, UniqueAdd.to_addOpposite, AddCon.orderIsoOp_symm_apply, AddOpposite.opMulEquiv_apply, AddLeftCancelMonoid.to_faithfulVAdd_addOpposite, AddAction.Regular.isPretransitive_addOpposite, AddUnits.continuous_embedProduct, AddOpposite.instVAddCommClass, AddOpposite.instNoZeroDivisors, Finset.addConvolution_op_vadd_eq_addConvolution_add_neg, AddOpposite.op_nsmul, AddSubmonoid.opEquiv_symm_apply, IsOpen.right_addCoset, AddOpposite.unop_neg, AddSubgroup.unop_le_unop_iff, AddOpposite.continuousConstVAdd, AddSubsemigroup.centerToAddOpposite_apply_coe, Set.image_op_zero, Set.image_op_neg, AddEquiv.op_symm_apply_apply, AddSubsemigroup.op_inf, AddUnits.isClosedEmbedding_embedProduct, IsClosed.right_addCoset, AddAction.right_quotientAction', Finset.image_op_nsmul, AddSubmonoid.unop_sup, AddSubmonoid.opEquiv_apply, AddSubmonoid.op_toSubsemigroup, isAddFundamentalDomain_Ioc', AddSubgroup.op_eq_top, Set.isCentralVAdd, Finset.addETransformRight_fst, AddOpposite.instIsRightCancelAdd, AddUnits.isEmbedding_embedProduct, IsAddRegular.op, UniqueSums.instAddOpposite, AddUnits.isInducing_embedProduct, AddSubsemigroup.coe_op, AddSubsemigroup.unop_closure, AddOpposite.comap_op_rightUniformSpace, VAddCommClass.op_left, AddOpposite.op_zero, AddSubmonoid.equivOp_symm_apply_coe, AddOpposite.opHomeomorph_symm_apply, QuotientAddGroup.orbit_mk_eq_vadd, measurableSMulβ_opposite_of_add, AddEquiv.op_apply_symm_apply, isAddRegular_op, Finset.image_op_neg, AddOpposite.addCommute_unop, Finset.neg_vadd_finset_distrib, uniformity_addOpposite, AddSubgroup.instCountableSubtypeAddOppositeMemOp, AddSubmonoid.centerToAddOpposite_apply_coe, Set.image_op_vadd_distrib, AddOpposite.instIsOrderedMonoid, AddSubmonoid.le_op_iff, IsAddUnit.op, AddSubgroup.equivOp_symm_apply_coe, AddOpposite.op_mul, AddMonoidHom.toOpposite_apply, AddOpposite.unop_add, AddOpposite.instLocallyCompactSpace, AddSubmonoid.op_bot, AddSubsemigroup.unop_eq_top, AddEquiv.op_apply_apply, AddOpposite.map_op_nhds
|
PreOpposite π | CompData | β |
Β«term_α΅α΅α΅Β» π | CompOp | β |
Β«term_α΅α΅α΅Β» π | CompOp | β |