| Name | Category | Theorems |
|---|
instAddCancelCommMonoid 📖 | CompOp | — |
instAddCancelMonoid 📖 | CompOp | — |
instAddCommGroup 📖 | CompOp | — |
instAddCommMonoid 📖 | CompOp | 1 mathmath: instIsOrderedAddMonoid
|
instAddCommSemigroup 📖 | CompOp | — |
instAddGroup 📖 | CompOp | 71 mathmath: AddSubgroup.centerToAddOpposite_apply_coe, comap_op_leftUniformSpace, AddAction.stabilizer_addSubgroup_op, AddSubgroup.normal_op, AddSubgroup.op_inf, AddSubgroup.coe_unop, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp, AddSubgroup.unop_normalizer, AddSubgroup.unop_sInf, AddSubgroup.op_le_iff, AddSubgroup.unop_closure, AddSubgroup.op_sInf, AddSubgroup.op_normalizer, AddSubgroup.unop_inf, AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, AddAction.stabilizer_op_addSubgroup, AddSubgroup.op.instNormal, AddSubgroup.le_op_iff, AddSubgroup.unop_iSup, AddSubgroup.op_top, AddSubgroup.op_toAddSubmonoid, AddSubgroup.op_le_op_iff, AddSubgroup.op_bot, AddSubgroup.unop_injective, AddSubgroup.op_toSubsemigroup, AddSubgroup.vadd_opposite_add, AddSubgroup.op_sup, AddSubgroup.op_closure, AddSubgroup.unop_toSubsemigroup, QuotientAddGroup.sound, AddSubgroup.unop_sup, AddSubgroup.coe_op, AddSubgroup.mem_op, AddSubgroup.isAddQuotientCoveringMap, AddSubgroup.opEquiv_symm_apply, AddSubgroup.op_sSup, instProperVAddAddOppositeOfIsTopologicalAddGroup, AddSubgroup.unop_eq_top, AddSubgroup.Normal.op, AddSubgroup.unop_eq_bot, instIsTopologicalAddGroupAddOpposite, AddSubgroup.unop_bot, AddSubgroup.op_iInf, AddSubgroup.unop_iInf, instIsUniformAddGroup, AddSubgroup.opEquiv_apply, AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite, AddSubgroup.op_injective, AddSubgroup.centerToAddOpposite_symm_apply_coe, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, QuotientAddGroup.orbit_eq_out_vadd, AddSubgroup.Normal.of_unop, AddAction.right_quotientAction, AddSubgroup.op_iSup, AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, AddSubgroup.unop_toAddSubmonoid, AddSubgroup.unop_top, AddSubgroup.mem_unop, AddSubgroup.equivOp_apply_coe, AddSubgroup.op_eq_bot, AddSubgroup.unop_sSup, AddSubgroup.vadd_opposite_image_add_preimage, AddSubgroup.normal_unop, instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe, AddSubgroup.unop_le_unop_iff, isAddFundamentalDomain_Ioc', AddSubgroup.op_eq_top, comap_op_rightUniformSpace, QuotientAddGroup.orbit_mk_eq_vadd, AddSubgroup.instCountableSubtypeAddOppositeMemOp, AddSubgroup.equivOp_symm_apply_coe
|
instAddLeftCancelMonoid 📖 | CompOp | — |
instAddLeftCancelSemigroup 📖 | CompOp | — |
instAddMonoid 📖 | CompOp | 48 mathmath: AddSubgroup.vadd_opposite_image_add_preimage', rightAddCoset_zero, isAddUnit_unop, Finset.neg_op_vadd_finset_distrib, HahnSeries.addOppositeEquiv_symm_support, rightAddCoset_mem_rightAddCoset, AddUnits.coe_unop_opEquiv, Finset.op_vadd_stabilizer_of_no_doubling, Set.neg_op_vadd_set_distrib, HahnSeries.addOppositeEquiv_support, op_vadd_add, instErgodicVAddAddOppositeOfIsAddRightInvariant, op_vadd_coe_set, op_vadd_op_vadd, instAddTorsionFree, mem_rightAddCoset_iff, NormedAddGroup.to_isIsometricVAdd_right, isAddUnit_op, HahnSeries.addOppositeEquiv_orderTop, rightAddCoset_eq_iff, AddAction.op_vadd_set_stabilizer_subset, eq_addCosets_of_normal, Set.op_vadd_inter_nonempty_iff, Finset.op_vadd_addConvolution_eq_addConvolution_vadd, DomAddAct.mk_nsmul, exponent, HahnSeries.addOppositeEquiv_symm_orderTop, mem_own_rightAddCoset, HahnSeries.addOppositeEquiv_symm_leadingCoeff, HahnSeries.addOppositeEquiv_leadingCoeff, unop_nsmul, DomAddAct.symm_mk_nsmul, Finset.addETransformLeft_fst, Set.neg_vadd_set_distrib, HahnSeries.addOppositeEquiv_symm_apply_coeff, orbit_addSubgroup_eq_rightCoset, normal_iff_eq_addCosets, HahnSeries.addOppositeEquiv_apply, lipschitzAdd, AddUnits.coe_opEquiv_symm, Finset.addConvolution_op_vadd_eq_addConvolution_add_neg, op_nsmul, IsOpen.right_addCoset, IsClosed.right_addCoset, AddAction.right_quotientAction', Finset.addETransformRight_fst, Finset.neg_vadd_finset_distrib, IsAddUnit.op
|
instAddRightCancelMonoid 📖 | CompOp | — |
instAddRightCancelSemigroup 📖 | CompOp | — |
instAddSemigroup 📖 | CompOp | — |
instAddZero 📖 | CompOp | 6 mathmath: AddMonoidHom.fromOpposite_apply, isDedekindFiniteAddMonoid_iff, AddMonoidHom.op_symm_apply_apply, AddMonoidHom.op_apply_apply, instIsDedekindFiniteAddMonoid, AddMonoidHom.toOpposite_apply
|
instAddZeroClass 📖 | CompOp | 47 mathmath: AddUnits.embedProduct_injective, AddSubmonoid.unop_le_unop_iff, AddSubmonoid.unop_inf, AddSubmonoid.op_sup, AddSubmonoid.unop_eq_bot, AddSubmonoid.unop_iInf, AddSubmonoid.centerToAddOpposite_symm_apply_coe, AddSubmonoid.op_eq_top, AddSubmonoid.unop_bot, AddSubmonoid.equivOp_apply_coe, AddSubmonoid.op_eq_bot, AddSubmonoid.unop_top, AddSubmonoid.unop_iSup, AddSubmonoid.mem_op, AddSubmonoid.unop_sInf, AddSubmonoid.op_top, AddSubmonoid.unop_closure, AddSubmonoid.op_le_op_iff, AddSubmonoid.unop_sSup, AddSubmonoid.op_inf, AddSubmonoid.mem_unop, AddSubmonoid.coe_unop, AddSubmonoid.op_sSup, AddUnits.embedProduct_apply, AddSubmonoid.op_iSup, AddSubmonoid.op_sInf, AddUnits.range_embedProduct, AddSubmonoid.op_le_iff, AddSubmonoid.unop_injective, AddSubmonoid.unop_eq_top, AddSubmonoid.op_closure, AddSubmonoid.unop_toSubsemigroup, AddSubmonoid.op_injective, AddSubmonoid.coe_op, AddSubmonoid.op_iInf, AddUnits.continuous_embedProduct, AddSubmonoid.opEquiv_symm_apply, AddUnits.isClosedEmbedding_embedProduct, AddSubmonoid.unop_sup, AddSubmonoid.opEquiv_apply, AddSubmonoid.op_toSubsemigroup, AddUnits.isEmbedding_embedProduct, AddUnits.isInducing_embedProduct, AddSubmonoid.equivOp_symm_apply_coe, AddSubmonoid.centerToAddOpposite_apply_coe, AddSubmonoid.le_op_iff, AddSubmonoid.op_bot
|
instCommGroup 📖 | CompOp | — |
instCommMonoid 📖 | CompOp | 5 mathmath: Finset.unop_prod, unop_finsuppProd, op_finsuppProd, Finset.op_prod, instIsOrderedMonoid
|
instCommSemigroup 📖 | CompOp | — |
instDivInvMonoid 📖 | CompOp | — |
instGroup 📖 | CompOp | — |
instLeftCancelSemigroup 📖 | CompOp | — |
instMonoid 📖 | CompOp | — |
instMulOneClass 📖 | CompOp | — |
instRightCancelSemigroup 📖 | CompOp | — |
instSemigroup 📖 | CompOp | — |
instSubNegMonoid 📖 | CompOp | 5 mathmath: op_zsmul, DomAddAct.mk_zsmul, DomAddAct.symm_mk_zsmul, unop_zsmul, unop_sub
|
instSubtractionCommMonoid 📖 | CompOp | — |
instSubtractionMonoid 📖 | CompOp | — |
pow 📖 | CompOp | 2 mathmath: unop_pow, op_pow
|
| Name | Category | Theorems |
|---|
instAddCommGroup 📖 | CompOp | 1 mathmath: instFiniteDimensional
|
instAddCommMagma 📖 | CompOp | — |
instAddCommMonoid 📖 | CompOp | 85 mathmath: op_finsuppSum, coe_opLinearEquiv_symm, Submodule.comap_op_mul, Submodule.comap_op_pow, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, Submodule.LinearDisjoint.op, RingEquiv.mopMatrix_symm_apply, AlgHom.mulLeftRightMatrix.inv_comp, coe_opLinearEquiv_symm_addEquiv, RingEquiv.mopMatrix_apply, MonoidAlgebra.opRingEquiv_symm_apply, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Module.Basis.mulOpposite_apply, AddMonoidAlgebra.opRingEquiv_symm_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, Module.Basis.mulOpposite_is_orthonormal_iff, AlgHom.toLinearMap_toOpposite, finrank, Submodule.map_unop_mul, coe_opLinearEquiv_addEquiv, instFree, summable_unop, isometry_opLinearEquiv, Algebra.TensorProduct.opAlgEquiv_apply, IsAzumaya.mulLeftRight_comp_congr, AlgHom.mulLeftRight_apply, IsAzumaya.bij, Module.Basis.mulOpposite_repr_op, opContinuousLinearEquiv_symm_apply, Submodule.map_unop_pow, hasSum_unop, Submodule.equivOpposite_apply, counit_def, coe_opLinearEquiv_toLinearMap, Submodule.map_op_pow, instIsStablyFiniteRingMulOpposite, HasSum.op, opLinearEquiv_toAddEquiv, hasSum_op, Module.Finite.instMulOpposite, IsAzumaya.coe_tensorEquivEnd, Algebra.TensorProduct.opAlgEquiv_symm_apply, Submodule.linearDisjoint_op, CliffordAlgebra.toBaseChange_comp_reverseOp, instIsOrderedAddMonoid, Submodule.map_op_mul, tsum_unop, AlgHom.toLinearMap_fromOpposite, AddMonoidAlgebra.opRingEquiv_apply, Submodule.map_unop_one, Module.Basis.mulOpposite_repr_eq, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, op_geom_sum, isStablyFiniteRing_iff, Submodule.comap_unop_pow, rank, Algebra.TensorProduct.opAlgEquiv_tmul, TwoSidedIdeal.subtypeMop_apply, coe_opLinearEquiv, comul_def, summable_op, opLinearEquiv_symm_toAddEquiv, opContinuousLinearEquiv_apply, Submodule.equivOpposite_symm_apply, op_geom_sum₂, Submodule.comap_unop_one, Submodule.mulMap_op, TwoSidedIdeal.subtypeMop_injective, coe_opLinearEquiv_symm_toLinearMap, Submodule.comap_op_one, instModuleIsReflexive, Submodule.map_op_one, Finset.unop_sum, Algebra.TensorProduct.opAlgEquiv_symm_tmul, tsum_op, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, MonoidAlgebra.opRingEquiv_apply, unop_finsuppSum, Finset.op_sum, Submodule.comap_unop_mul, Module.Basis.repr_unop_eq_mulOpposite_repr, AlgHom.mulLeftRightMatrix.comp_inv, IsAzumaya.AlgHom.mulLeftRight_bij, Summable.op
|
instAddCommSemigroup 📖 | CompOp | — |
instAddGroup 📖 | CompOp | — |
instAddLeftCancelSemigroup 📖 | CompOp | — |
instAddMonoid 📖 | CompOp | — |
instAddRightCancelSemigroup 📖 | CompOp | — |
instAddSemigroup 📖 | CompOp | — |
instAddZeroClass 📖 | CompOp | 5 mathmath: AddMonoidHom.mulOp_apply_apply, NonUnitalRingHom.op_symm_apply_apply, AddMonoidHom.mul_op_ext_iff, NonUnitalRingHom.op_apply_apply, AddMonoidHom.mulOp_symm_apply_apply
|
instCancelCommMonoid 📖 | CompOp | — |
instCancelMonoid 📖 | CompOp | — |
instCommGroup 📖 | CompOp | — |
instCommMonoid 📖 | CompOp | 1 mathmath: instIsOrderedMonoid
|
instCommSemigroup 📖 | CompOp | — |
instDivInvMonoid 📖 | CompOp | 5 mathmath: unop_zpow, DomMulAct.mk_zpow, op_zpow, DomMulAct.symm_mk_zpow, unop_div
|
instDivisionCommMonoid 📖 | CompOp | — |
instDivisionMonoid 📖 | CompOp | — |
instGroup 📖 | CompOp | 74 mathmath: Subgroup.unop_inf, Subgroup.instCountableSubtypeMulOppositeMemOp, Subgroup.equivOp_symm_apply_coe, Subgroup.op_le_op_iff, Subgroup.op_iSup, Function.Embedding.instIsCentralScalar, RootPairing.range_weylGroup_coweightHom, Subgroup.op_bot, DomMulAct.mem_stabilizer_iff, Subgroup.op_iInf, Subgroup.unop_closure, Subgroup.unop_eq_bot, MulAction.right_quotientAction, Subgroup.mem_op, Subgroup.unop_normalizer, Subgroup.op_top, Subgroup.smul_diff_smul', Subgroup.centerToMulOpposite_apply_coe, Subgroup.Normal.of_unop, Subgroup.op_inf, Subgroup.smul_opposite_image_mul_preimage, Subgroup.normal_op, Subgroup.op_normalizer, Subgroup.op_toSubsemigroup, instIsUniformGroup, Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp, instIsTopologicalGroupMulOpposite, Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite, ValuationSubring.pointwise_central_scalar, MulAction.stabilizer_subgroup_op, Subgroup.Normal.op, Subgroup.unop_sInf, MulAction.stabilizer_op_subgroup, QuotientGroup.orbit_eq_out_smul, Subgroup.op_eq_top, Subgroup.op_sInf, Subgroup.unop_toSubsemigroup, Subgroup.coe_unop, Subgroup.equivOp_apply_coe, Subgroup.smul_opposite_mul, Subgroup.opEquiv_symm_apply, Subgroup.unop_eq_top, Subgroup.unop_iSup, DomMulAct.stabilizerMulEquiv_apply, comap_op_leftUniformSpace, Subgroup.unop_injective, instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe, Subgroup.op_closure, Subgroup.op_injective, Subgroup.op_sup, instProperSMulMulOppositeOfIsTopologicalGroup, Subgroup.unop_sSup, Subgroup.unop_bot, QuotientGroup.orbit_mk_eq_smul, Subgroup.op_toSubmonoid, Subgroup.coe_op, comap_op_rightUniformSpace, Subgroup.op_eq_bot, Subgroup.le_op_iff, Subgroup.unop_le_unop_iff, Subgroup.op.instNormal, Subgroup.op_sSup, Subgroup.mem_unop, Subgroup.centerToMulOpposite_symm_apply_coe, Subgroup.unop_sup, Subgroup.op_le_iff, Subgroup.normal_unop, Subgroup.smul_diff', QuotientGroup.sound, Subgroup.unop_toSubmonoid, Subgroup.unop_iInf, Subgroup.isQuotientCoveringMap, Subgroup.opEquiv_apply, Subgroup.unop_top
|
instLeftCancelMonoid 📖 | CompOp | — |
instLeftCancelSemigroup 📖 | CompOp | — |
instMonoid 📖 | CompOp | 186 mathmath: DoubleCoset.doubleCoset_union_rightCoset, AddOpposite.instMulTorsionFree, HasStrictFDerivAt.fun_mul', NormedGroup.to_isIsometricSMul_right, hasStrictFDerivAt_list_prod_finRange', TrivSqZeroExt.lift_inlAlgHom_inrHom, mem_own_rightCoset, TrivSqZeroExt.snd_pow_eq_sum, MeasureTheory.integral_domSMul, MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, fderivWithin_fun_pow', MulAction.right_quotientAction', DomMulAct.symm_mk_pow, Finset.inv_smul_finset_distrib, Finset.doubling_lt_three_halves, TrivSqZeroExt.inv_inl, MeasureTheory.Measure.domSMul_apply, TrivSqZeroExt.inv_one, CategoryTheory.Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, HasStrictFDerivAt.mul', MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv, TrivSqZeroExt.snd_list_prod, TrivSqZeroExt.fstHom_comp_map, fderiv_fun_pow', MeasureTheory.Measure.IsAddHaarMeasure.domSMul, Finset.inv_op_smul_finset_distrib, rightCoset_eq_iff, Monoid.CoprodI.inv_def, DualNumber.inv_eps, HasStrictFDerivAt.list_prod', MulAction.op_smul_set_stabilizer_subset, CategoryTheory.End.smul_left, NormMulClass.toNormSMulClass_op, TrivSqZeroExt.fst_invOf, Finset.smul_inv_mul_eq_inv_mul_opSMul, exponent, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar, TrivSqZeroExt.map_comp_inlAlgHom, MeasureTheory.Measure.addHaarScalarFactor_smul_congr, fderiv_mul_const', TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf, TrivSqZeroExt.inl_mul_inr, Subgroup.smul_diff_smul', TrivSqZeroExt.fst_list_prod, isUnit_op, MeasureTheory.distribHaarChar_apply, TrivSqZeroExt.mul_left_eq_one, CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, fderiv_pow', CategoryTheory.Mat.equivalenceSingleObjInverse_obj_carrier, AddSubmonoid.pointwise_isCentralScalar, op_smul_coe_set, op_pow, TrivSqZeroExt.inr_mul_inr, Subgroup.pointwise_isCentralScalar, fderivWithin_fun_mul', Subsemiring.pointwise_central_scalar, hasFDerivAt_list_prod', fderiv_mul', DualNumber.exists_mul_left_or_mul_right, unop_pow, TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf, hasFDerivWithinAt_pow', TrivSqZeroExt.mul_inv_cancel, AffineMap.isCentralScalar, RingEquiv.moduleEndSelf_apply, TrivSqZeroExt.inv_mul_cancel, fderivWithin_mul_const', hasFDerivAt_list_prod_finRange', TrivSqZeroExt.invOf_eq_inv, normal_iff_eq_cosets, MeasureTheory.Measure.Regular.domSMul, TrivSqZeroExt.inl_mul, op_smul_op_smul, MeasureTheory.Measure.instSMulCommClassDomMulActNNReal, Set.op_smul_inter_nonempty_iff, HasFDerivWithinAt.mul_const', AddMonoid.End.isCentralScalar, Units.coe_unop_opEquiv, IsTopologicalSemiring.toOppositeIsModuleTopology, fderiv_pow_ring', lipschitzMul, DoubleCentralizer.instIsCentralScalar, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, TrivSqZeroExt.inv_inv, HasFDerivAt.fun_pow', HasMFDerivWithinAt.mul', isUnit_unop, TrivSqZeroExt.inr_mul_inl, TrivSqZeroExt.snd_invOf, TrivSqZeroExt.inl_mul_inl, MeasureTheory.Measure.instSMulCommClassNNRealDomMulAct, hasStrictFDerivAt_pow', LieSubmodule.Quotient.isCentralScalar, fderiv_fun_mul', Derivation.instIsCentralScalar, Set.inv_smul_set_distrib, IsOpen.rightCoset, TrivSqZeroExt.isUnit_inv_iff, Subring.pointwise_central_scalar, rightCoset_mem_rightCoset, TrivSqZeroExt.inv_neg, Submonoid.pointwise_isCentralScalar, hasStrictFDerivAt_list_prod_attach', MeasureTheory.Lp.instIsCentralScalar, Matrix.scalar_comm_iff, Finset.op_smul_convolution_eq_convolution_smul, HasFDerivWithinAt.pow', HasFDerivAt.list_prod', hasFDerivAt_pow', DualNumber.commute_eps_left, Subgroup.smul_opposite_image_mul_preimage', CategoryTheory.Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, StarSemigroup.toOpposite_starModule, Finset.mulETransformRight_fst, orbit_subgroup_eq_rightCoset, op_geom_sum, DualNumber.commute_eps_right, Set.inv_op_smul_set_distrib, HasFDerivAt.pow', HasStrictFDerivAt.pow', CentroidHom.instIsCentralScalar, HasStrictFDerivAt.mul_const', Units.coe_opEquiv_symm, DomMulAct.mk_pow, Ideal.pointwise_central_scalar, fderivWithin_list_prod', FreeLieAlgebra.instIsCentralScalar, HasFDerivWithinAt.fun_mul', ContinuousAlternatingMap.instIsCentralScalar, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, instErgodicSMulMulOppositeOfIsMulRightInvariant, fderivWithin_pow_ring', eq_cosets_of_normal, HasFDerivWithinAt.fun_pow', CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, MeasureTheory.Measure.addHaarScalarFactor_domSMul, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, HasFDerivAt.mul_const', HasStrictFDerivAt.fun_pow', Finset.op_smul_stabilizer_of_no_doubling, DualNumber.lift_op_smul, TrivSqZeroExt.mul_right_eq_one, CategoryTheory.Mat.equivalenceSingleObjInverse_map, op_geom_sum₂, MeasureTheory.Measure.addHaarScalarFactor_smul_congr', TrivSqZeroExt.inl_mul_eq_smul, hasStrictFDerivAt_list_prod', TrivSqZeroExt.inv_zero, Ring.uniformContinuousConstSMul_op, DualNumber.eps_mul_eps, IsUnit.op, ContinuousLinearMap.isCentralScalar, rightCoset_one, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_str, HasFDerivWithinAt.mul', DualNumber.snd_mul, fderivWithin_mul', RestrictScalars.isCentralScalar, mem_rightCoset_iff, TrivSqZeroExt.mul_inv_rev, Matrix.scalar_commute_iff, fderiv_list_prod', HasMFDerivAt.mul', RootPairing.Equiv.instSMulCommClassMulOppositeAut, AddSubgroup.pointwise_isCentralScalar, HasFDerivAt.fun_mul', LieSubalgebra.instIsCentralScalarSubtypeMem, HasFDerivAt.mul', hasFDerivAt_list_prod_attach', Subgroup.smul_diff', Matrix.op_smul_eq_vecMul, Finset.mulETransformLeft_fst, TrivSqZeroExt.mul_inl_eq_op_smul, op_smul_mul, ContinuousAffineMap.instIsCentralScalar, TrivSqZeroExt.inv_inr, Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves, TensorProduct.instIsCentralScalar, AlternatingMap.instIsCentralScalar, Submodule.pointwiseCentralScalar, IsClosed.rightCoset, HasFDerivWithinAt.list_prod', TwoSidedIdeal.coe_mop_smul, Finset.convolution_op_smul_eq_convolution_mul_inv, fderivWithin_pow'
|
instMulOne 📖 | CompOp | 19 mathmath: Monoid.Foldl.ofFreeMonoid_apply, Traversable.foldlm.ofFreeMonoid_comp_of, Monoid.CoprodI.inv_def, RootPairing.Equiv.coweightHom_injective, RootPairing.Hom.coweightHom_injective, instIsStablyFiniteRingMulOpposite, MonoidHom.op_symm_apply_apply, Traversable.foldl.unop_ofFreeMonoid, Monoid.foldlM.ofFreeMonoid_apply, RootPairing.Equiv.coweightHom_op, isStablyFiniteRing_iff, Traversable.foldl.ofFreeMonoid_comp_of, isDedekindFiniteMonoid_iff, MonoidHom.op_apply_apply, instIsDedekindFiniteMonoid, RootPairing.Equiv.coweightHom_toLinearMap, MonoidHom.toOpposite_apply, RootPairing.Equiv.coweightHom_apply, MonoidHom.fromOpposite_apply
|
instMulOneClass 📖 | CompOp | 58 mathmath: Submonoid.le_op_iff, Submonoid.equivOp_symm_apply_coe, Submonoid.op_iInf, Submonoid.unop_eq_top, Subring.addEquivOp_apply_coe, Submonoid.unop_iInf, Submonoid.unop_iSup, Submonoid.unop_inf, RootPairing.range_weylGroup_coweightHom, Monoid.CoprodI.inv_def, Subsemiring.addEquivOp_apply_coe, Submonoid.op_eq_bot, Submonoid.centerToMulOpposite_apply_coe, Submonoid.op_sSup, Submonoid.op_sInf, Submonoid.unop_top, Subsemiring.addEquivOp_symm_apply_coe, Submonoid.op_iSup, Submonoid.coe_op, Submonoid.centerToMulOpposite_symm_apply_coe, Submonoid.op_le_iff, Units.isEmbedding_embedProduct, Submonoid.op_sup, Submonoid.unop_eq_bot, Submonoid.unop_le_unop_iff, Submonoid.op_le_op_iff, Submonoid.unop_sup, Submonoid.equivOp_apply_coe, Submonoid.op_inf, Submonoid.unop_sInf, Subring.ringEquivOpMop_symm_apply_coe, Submonoid.opEquiv_apply, Subsemiring.ringEquivOpMop_symm_apply_coe, Submonoid.unop_sSup, Submonoid.op_eq_top, Submonoid.unop_bot, Units.isClosedEmbedding_embedProduct, Submonoid.op_closure, Units.continuous_embedProduct, Submonoid.op_injective, Submonoid.unop_injective, Submonoid.mem_op, Subalgebra.linearEquivOp_symm_apply_coe, Submonoid.mem_unop, Units.embed_product_star, Submonoid.unop_closure, Submonoid.coe_unop, Subalgebra.algEquivOpMop_symm_apply_coe, Submonoid.op_top, Units.range_embedProduct, Units.embedProduct_injective, Submonoid.op_bot, Submonoid.opEquiv_symm_apply, Units.isInducing_embedProduct, Subring.addEquivOp_symm_apply_coe, Submonoid.unop_toSubsemigroup, Units.embedProduct_apply, Submonoid.op_toSubsemigroup
|
instRightCancelMonoid 📖 | CompOp | — |
instRightCancelSemigroup 📖 | CompOp | — |
instSemigroup 📖 | CompOp | — |
instSubNegMonoid 📖 | CompOp | — |