Defs

📁 Source: Mathlib/Algebra/Notation/Pi/Defs.lean

Statistics

Metric	Count
Definitions instAdd, instDiv, instInv, instMul, instNeg, instOne, instPow, instSMul, instStarForall, instSub, instVAdd, instZero, prod	13
Theorems const_add, const_div, const_inv, const_mul, const_neg, const_one, const_pow, const_sub, const_zero, smul_const, vadd_const, add_apply, add_comp, add_def, comp_one, comp_zero, div_apply, div_comp, div_def, inv_apply, inv_comp, inv_def, mul_apply, mul_comp, mul_def, neg_apply, neg_comp, neg_def, one_apply, one_comp, one_def, pow_apply, pow_comp, pow_def, prod_fst_snd, prod_snd_fst, smul_apply, smul_comp, smul_def, star_apply, star_def, sub_apply, sub_comp, sub_def, vadd_apply, vadd_comp, vadd_def, zero_apply, zero_comp, zero_def	50
Total	63

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_add 📖	mathematical	—	Pi.instAdd	—	—
const_div 📖	mathematical	—	Pi.instDiv	—	—
const_inv 📖	mathematical	—	Pi.instInv	—	—
const_mul 📖	mathematical	—	Pi.instMul	—	—
const_neg 📖	mathematical	—	Pi.instNeg	—	—
const_one 📖	mathematical	—	Pi.instOne	—	—
const_pow 📖	mathematical	—	Pi.instPow	—	—
const_sub 📖	mathematical	—	Pi.instSub	—	—
const_zero 📖	mathematical	—	Pi.instZero	—	—
smul_const 📖	mathematical	—	Pi.instSMul	—	—
vadd_const 📖	mathematical	—	HVAdd.hVAdd instHVAdd Pi.instVAdd	—	—

Pi

Definitions

Name	Category	Theorems
instAdd 📖	CompOp	775 math math: MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add, MeasureTheory.predictablePart_add_ae_eq, Filter.BoundedAtFilter.add, RingEquiv.piCongrRight_apply, DFinsupp.liftAddHom_apply, MeasureTheory.setToFun_add_left, Fintype.balance_add, Set.indicator_self_add_compl, Finset.noncommSum_add_distrib_aux, conjneg_add, MDifferentiable.add, isAddRegular_iff, ContDiffMapSupportedIn.coe_add, HasMFDerivAt.add, MeasureTheory.UnifTight.add, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left, birkhoffAverage_add, instCanonicallyOrderedAddForall, Derivation.coe_add, MDifferentiableWithinAt.add, HasFDerivWithinAt.add, LinearGrowth.linearGrowthInf_add_le', Rep.diagonalSuccIsoFree_inv_hom_single, Nat.isLinearSet_iff_exists_matrix, EReal.liminf_add_top_of_ne_bot, LinearGrowth.le_linearGrowthSup_add, AddHom.coeFn_apply, AddEquiv.piAdditive_apply, DFinsupp.liftAddHom_apply_single, ProbabilityTheory.covariance_add_left, NumberField.mixedEmbedding.convexBodySumFun_add_le, ValueDistribution.characteristic_mul_top_le, addCommute_iff, HasFPowerSeriesOnBall.add, Matrix.vec_add, WithCStarModule.add_apply, Rep.leftRegularHom_hom, LinearGrowth.linearGrowthSup_add_le, Differentiable.add_iff_right, MeasureTheory.IsStoppingTime.add, MeasureTheory.Lp.coeFn_add, MeasureTheory.TendstoInDistribution.add_of_tendstoInMeasure_const, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, VectorField.mpullbackWithin_add, IsAddFreimanHom.add, MeasureTheory.condLExp_add_right, MeasureTheory.lpNorm_add_le', ValueDistribution.logCounting_zero_mul_le, Matrix.entryAddHom_eq_comp, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', Matrix.det_updateRow_add_self, ProbabilityTheory.Kernel.coe_add, DifferentiableWithinAt.add, Matrix.add_mulVec, AEMeasurable.add', ValueDistribution.proximity_zero_mul_le, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Measurable.add_simpleFunc, AbsolutelyContinuousOnInterval.add, MulEquiv.piMultiplicative_apply, Asymptotics.IsLittleO.right_isTheta_add, mdifferentiableAt_add_section, MeasureTheory.Integrable.add', MeasureTheory.StronglyMeasurable.add_iff_right, CPolynomialAt.add, MultilinearMap.piFamily_add, Matrix.toMvPolynomial_add, meromorphicOrderAt_add_of_ne, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀', QuadraticMap.polar_add, le_limsup_add, LieDerivation.coe_add, ProbabilityTheory.Kernel.iIndepFun.indepFun_add_add, Asymptotics.IsBigOTVS.add, Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply, Matrix.add_cons, HahnSeries.SummableFamily.coe_add, LieModule.genWeightSpaceChain_def', AddEquiv.val_neg_piAddUnits_apply, LinearGrowth.le_linearGrowthSup_add', AddEquiv.funUnique_symm_apply, ConvexOn.univ_sSup_of_countable_affine_eq, MeasureTheory.Adapted.add, MeasureTheory.eLpNorm_add_lt_top, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, ExpGrowth.expGrowthSup_add, HasFPowerSeriesAt.add, ContDiffWithinAt.laplacianWithin_add, MeromorphicOn.add, Set.indicator_symmDiff, FreeAbelianGroup.lift_add, Measurable.add', AddEquiv.piUnique_apply, MeasureTheory.Measure.instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite, RingEquiv.piOptionEquivProd_apply, RingEquiv.piCongrLeft_symm_apply, AEMeasurable.add_iff_right, ConcaveOn.add_const, ProbabilityTheory.iIndepFun.indepFun_add_left₀, BoxIntegral.integral_add, AddGroupNorm.coe_add, HolderWith.add, Function.extend_add, RingEquiv.piCongrLeft'_symm, Matrix.det_updateRow_add_smul_self, RingEquiv.piCongrLeft'_apply, MeasureTheory.condLExp_add_left, ContinuousAt.add, HasDerivAtFilter.add, CentroidHom.coe_add, Asymptotics.IsLittleO.add_isTheta, ContinuousMapZero.coe_add, Finsupp.llift_apply, measurableAdd, ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right₀, EReal.iSup_add_le_add_iSup, MeromorphicOn.extract_zeros_poles_log, Function.mulSupport_one_add', ValueDistribution.logCounting_add_top_le, analyticOrderAt_add_eq_left_of_lt, ContinuousAffineMap.decomp, TendstoLocallyUniformlyOn.add, ContMDiffWithinAt.add_section, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, ContMDiffAt.add_section, Asymptotics.IsEquivalent.add_add_of_nonneg, MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite, MeasureTheory.L1.SimpleFunc.setToL1S_add_left, ValueDistribution.logCounting_mul_zero_eventuallyLE, Matrix.updateRow_eq_transvection, AddHom.compLeft_apply, Matrix.submatrix_add, MeasureTheory.SimpleFunc.coe_add, Finsupp.liftAddHom_comp_single, ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left₀, Filter.Tendsto.uniformity_add_iff_right, Asymptotics.IsEquivalent.add_isLittleO, HasDerivAt.add, ValueDistribution.logCounting_mul_top_eventuallyLE, BoxIntegral.integralSum_add, Asymptotics.IsTheta.add_isLittleO, Matrix.coe_ofAddEquiv_symm, HasFDerivAt.add, ProbabilityTheory.IndepFun.add_hasPDF', iteratedFDeriv_add_apply, LieModule.coe_chainTop, DifferentiableAt.add_iff_left, ENNReal.essSup_add_le, extDerivWithin_add, Matrix.piRingEquiv_apply, UniformCauchySeqOn.add, MDifferentiableAt.add, isSemisimpleRing_iff_pi_matrix_divisionRing, Matrix.vec3_add, MeasureTheory.SimpleFunc.setToSimpleFunc_add_left, MeasureTheory.lpNorm_add_le, Fintype.piFinset_add, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, MeasureTheory.integral_exp_tilted, meromorphicOrderAt_add_eq_left_of_lt, Matrix.vecMulVec_add, meromorphicOrderAt_add, FormalMultilinearSeries.ofScalars_add, Matrix.entryAddMonoidHom_eq_comp, single_add, Filter.isCoboundedUnder_ge_add, ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add, MeasureTheory.OuterMeasure.coe_add, FreeAbelianGroup.liftAddEquiv_symm_apply, Matrix.vecMul_fromRows, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_add, Matrix.of_add_of, LinearEquiv.funUnique_symm_apply, ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left, Matrix.piRingEquiv_symm_apply, MeasureTheory.Submartingale.add_martingale, Matrix.piLinearEquiv_apply, VectorField.mpullback_add_apply, RingEquiv.piCongrRight_refl, Matrix.circulant_add, Matrix.det_updateRow_sum_aux, MeasureTheory.FinMeasAdditive.add, MeasureTheory.lpNorm_le_add_lpNorm_add, ContinuousAffineMap.coe_add, instIsLeftCancelAdd, MeasureTheory.Martingale.add, Matrix.blockDiag_add, MultilinearMap.dfinsuppFamily_add, cross_anticomm', RingEquiv.piEquivPiSubtypeProd_symm_apply, ProbabilityTheory.HasGaussianLaw.add, Asymptotics.SuperpolynomialDecay.add, Set.indicator_compl', MeasureTheory.integrable_add_iff_of_nonneg, IsCompactOperator.add, LinearMap.toMvPolynomial_add, Filter.Tendsto.conj_nhds_zero, LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero, InnerProductSpace.HarmonicOnNhd.add, UnitAddTorus.mFourier_add, MeasureTheory.LocallyIntegrableOn.add, ProbabilityTheory.iCondIndepFun.indepFun_add_left, Int.addSubgroup_index_ne_zero_iff, Finsupp.comp_liftAddHom, AddEquiv.piUnique_symm_apply, liminf_add_le, AddEquiv.funUnique_apply, ConvexOn.sSup_of_countable_affine_eq, ContinuousMultilinearMap.map_piecewise_add, ProbabilityTheory.iIndepFun.hasGaussianLaw_add, Filter.isBoundedUnder_le_add, ContDiffAt.laplacian_add, MeasureTheory.IntegrableAtFilter.add, ValueDistribution.proximity_sum_top_le, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf', MeasureTheory.Lp.simpleFunc.add_toSimpleFunc, MeasureTheory.Supermartingale.add_martingale, VectorFourier.fourierIntegral_add, MonovaryOn.add_right, MeasureTheory.Submartingale.add, Matrix.det_updateCol_add, ProbabilityTheory.Kernel.integral_integral_add', Finsupp.lift_apply, AnalyticWithinAt.add, MeasureTheory.Measure.add_comp', MeasureTheory.LocallyIntegrable.add, Seminorm.coe_add, MeasureTheory.MemLp.add, StrictConvexOn.add, ConvexOn.add_strictConvexOn, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, isAddRightRegular_iff, ConvexOn.real_univ_sSup_of_countable_affine_eq, Rep.indResAdjunction_counit_app_hom_hom, Matrix.vecMul_fromBlocks, UniformConcaveOn.sub, MeasureTheory.Measure.pi.isAddRightInvariant, ValueDistribution.proximity_mul_zero_le, EReal.le_liminf_add, lp.coeFn_add, IncidenceAlgebra.coe_add, Function.mulSupport_add_one', Matrix.schur_complement_eq₂₂, ProbabilityTheory.covariance_add_right, MeasureTheory.setToFun_add, ContinuousMultilinearMap.map_add_univ, MeasureTheory.withDensity_add_left, Filter.Tendsto.uniformity_add_iff_left, QuadraticMap.coeFn_add, ValueDistribution.proximity_add_top_le, MeasureTheory.Measure.rnDeriv_add, NumberField.mixedEmbedding.normAtPlace_add_le, Matrix.replicateRow_add, Set.indicator_add', MeasureTheory.tilted_tilted, MDifferentiableOn.add, EReal.liminf_add_le, addHom_apply, RingEquiv.piEquivPiSubtypeProd_apply, BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg, ValueDistribution.logCounting_add_analyticOn, AddMonoidAlgebra.coe_add, Matrix.fromBlocks_mulVec, Measurable.stronglyMeasurable_add, MeasureTheory.condExpL1_add, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left, MeasureTheory.integrable_add_of_disjoint, AddEquiv.arrowCongr_apply, MemHolder.add, MultilinearMap.map_add_sub_map_add_sub_linearDeriv, MeasureTheory.AEStronglyMeasurable.add, VectorField.leibniz_identity_mlieBracket, ProbabilityTheory.iCondIndepFun.indepFun_add_right, AddGroupSeminorm.coe_add, iteratedDeriv_add, Filter.EventuallyConst.add, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf, Measurable.add_stronglyMeasurable, ConvexOn.sSup_of_nat_affine_eq, DFinsupp.coe_add, LieModule.exists₂_genWeightSpace_smul_add_eq_bot, Matrix.empty_add_empty, LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, Set.indicator_diff', UniformConvexOn.add, mfderiv_add, LSeriesHasSum.add, VectorField.mlieBracketWithin_add_left, VectorField.lieBracket_add_left, DifferentiableOn.add_iff_right, meromorphicOrderAt_add_of_top_left, Function.HasTemperateGrowth.add, iteratedFDeriv_add, MeasureTheory.Measure.coe_add, ValueDistribution.characteristic_add_top_eventuallyLE, BoundedContinuousFunction.coe_add, MonoidAlgebra.coe_add, AntivaryOn.add_left, HasStrictFDerivAt.add, MeasureTheory.stoppedProcess_eq, Matrix.cons_add_cons, AddEquiv.piCongrRight_symm, Filter.isCoboundedUnder_le_add, ContinuousLinearMap.coe_add', ContMDiffMap.coe_add, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, Matrix.add_vecMul, MeasureTheory.AEFinStronglyMeasurable.add, Complex.ofReal_comp_add, AEMeasurable.add_iff_left, OnePoint.IsZeroAt.add, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, HasStrictDerivAt.add, ContMDiff.add, Filter.Tendsto.uniformity_add, AddEquiv.piAdditive_symm_apply, VectorField.mlieBracket_add_right, Matrix.tail_add, mdifferentiableWithinAt_add_section, Antivary.add_right, ValueDistribution.logCounting_add_top_eventuallyLE, CauchySeq.add, HasDerivWithinAt.add, ContMDiffWithinAt.add, ValueDistribution.logCounting_mul_top_le, Finsupp.liftAddHom_apply, ENNReal.lintegral_Lp_add_le, iteratedFDerivWithin_add_apply, MeasureTheory.condExp_add, instIsRightCancelAdd, Function.Even.add, ENNReal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top, map_comp_add, MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₂, Differentiable.add_iff_left, Poly.coe_add, ValueDistribution.proximity_mul_top_le, translate_add_right, add_def, AddEquiv.piCongrRight_refl, ValueDistribution.characteristic_mul_zero_eventuallyLE, Hamming.toHamming_add, ValueDistribution.characteristic_top_mul_le, MvPowerSeries.HasEval.add, ValueDistribution.logCounting_top_mul_eventually_le, OrderAddMonoidHom.coe_add, HasCompactSupport.add, analyticOrderAt_add_eq_right_of_lt, TendstoUniformly.add, LeftInvariantDerivation.coe_add, ContMDiffOn.add_section, MeasureTheory.martingalePart_add_predictablePart, ProbabilityTheory.IndepFun.cgf_add, LSeriesSummable.add, Antivary.add_left, LSeries.abscissaOfAbsConv_add_le, TestFunction.coe_add, Set.MapsTo.add, Nat.isSemilinearSet_setOf_mulVec_eq, RingEquiv.sumArrowEquivProdArrow_symm_apply, SchwartzMap.smulLeftCLM_add, add_apply, AnalyticAt.add, Function.Periodic.cuspFunction_add, extDeriv_add, Tactic.ComputeAsymptotics.Majorized.add, instIsCancelAdd, ContMDiffSection.coe_add, DifferentiableOn.add_iff_left, fwdDiff_iter_add, LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add, MeasureTheory.integrable_add_iff_of_nonpos, Matrix.piAddEquiv_symm_apply, UniformConcaveOn.add, LieModule.genWeightSpace_le_genWeightSpaceChain, MeasureTheory.stoppedProcess_eq'', leibniz_cross, MeromorphicAt.add, MultilinearMap.map_add_eq_map_add_linearDeriv_add, ContinuousAlternatingMap.map_add_univ, ValueDistribution.characteristic_add_top_le, Matrix.blockDiag'_add, Matrix.schur_complement_eq₁₁, qExpansion_add, EReal.add_iInf_le_iInf_add, MeasureTheory.VectorMeasure.coe_add, Hamming.ofHamming_add, VectorField.mlieBracket_add_left, AddHom.coe_add, ContDiffAt.laplacian_add_nhds, MeasureTheory.FinStronglyMeasurable.add, HasFTaylorSeriesUpToOn.add, continuousAdd', le_analyticOrderAt_add, ExpGrowth.le_expGrowthInf_add, List.aestronglyMeasurable_sum, ConvexOn.real_univ_sSup_affine_eq, LieAlgebra.toEnd_pow_apply_mem, fderiv_add, TwoUniqueSums.instForall, PolynomialLaw.add_def, RingEquiv.piUnique_symm_apply, ValueDistribution.characteristic_mul_zero_le, Finsupp.coe_add, LSeries.term_add_apply, Measurable.simpleFunc_add, ProbabilityTheory.iIndepFun.indepFun_add_add, Function.const_add, Sigma.uncurry_add, Matrix.vecMul_add, LieModule.exists_genWeightSpace_smul_add_eq_bot, MeasureTheory.FiniteMeasure.coeFn_add, TemperedDistribution.smulLeftCLM_add, MultilinearMap.map_piecewise_add, ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun, fwdDiff_smul, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₁, Matrix.vec2_add, AnalyticOn.add, cuspFunction_add, add_dotProduct, ValueDistribution.logCounting_zero_mul_eventually_le, LieModuleHom.coe_add, HasFDerivAtFilter.add, Finset.piAntidiag_cons, ProbabilityTheory.iIndepFun.indepFun_add_mul₀, MeasureTheory.eLpNormEssSup_add_le, Matrix.blockDiagonal'_add, Module.rankAtStalk_prod, add_bounded_of_bounded_of_bounded, ContinuousMap.coe_add, MeasureTheory.ConvolutionExistsAt.add_distrib, birkhoffSum_add', MeasureTheory.AEStronglyMeasurable.add_iff_left, ProbabilityTheory.iIndepFun.indepFun_add_right₀, MeasureTheory.AEEqFun.coeFn_add, VectorField.mlieBracketWithin_add_right, single_apply_addCommute, IsSemisimpleModule.exists_end_ringEquiv, GroupNorm.coe_add, MeasureTheory.stoppedProcess_eq_of_mem_finset, ConcaveOn.add, TendstoLocallyUniformly.add, LieModule.genWeightSpaceChain_def, LSeries.term_add, MeasureTheory.memLp_add_of_disjoint, List.aemeasurable_sum, NumberField.mixedEmbedding.logMap_unit_smul, LieModule.chainTopCoeff_add_one, Matrix.blockDiagonal_add, Matrix.mulVec_add, ProbabilityTheory.iIndepFun.indepFun_add_left, AdicCompletion.val_add, Submodule.quotientPi_aux.map_add, HasMFDerivWithinAt.add, linearIndependent_add_smul_iff, MeasureTheory.exists_Lp_half, RingEquiv.piCongrLeft_apply, MeasureTheory.StronglyMeasurable.add_iff_left, Set.indicator_add_compl_eq_piecewise, curveIntegralFun_add, Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding, MeasureTheory.withDensityᵥ_add, Function.Periodic.add, ProbabilityTheory.variance_add, Finsupp.linearCombination_comp_addSingleEquiv, CPolynomialOn.add, PolynomialLaw.toFun_add, LSeries_add, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, ProbabilityTheory.IndepFun.variance_add, DFinsupp.comp_liftAddHom, MeasureTheory.eLpNorm'_add_le_of_le_one, ENNReal.limsup_add_of_right_tendsto_zero, add_comp, ConvexOn.univ_sSup_affine_eq, Cardinal.sum_add_distrib, AffineMap.decomp, ConvexOn.real_univ_sSup_of_nat_affine_eq, Set.piecewise_add, Matrix.add_vecMulVec, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, addHom_injective, Finset.noncommSum_add_distrib, HasFiniteFPowerSeriesOnBall.add, Filter.Germ.coe_add, ProbabilityTheory.Kernel.withDensity_add_right, single_add_single_eq_single_add_single, Matrix.diag_add, Representation.IntertwiningMap.coe_add, ConvexOn.real_sSup_of_countable_affine_eq, MvPowerSeries.HasSubst.add, ValueDistribution.characteristic_zero_mul_eventually_le, VectorField.lieBracketWithin_add_left, VectorField.mpullback_add, LieModule.eventually_genWeightSpace_smul_add_eq_bot, LieModule.coe_chainBot, UniqueSums.instForall, ProbabilityTheory.iCondIndepFun.indepFun_add_add, TendstoUniformlyOnFilter.add, Meromorphic.add, AffineMap.coe_add, AnalyticOnNhd.add, ENNReal.liminf_add_of_right_tendsto_zero, MemHolder.nnHolderNorm_add_le, List.periodic_sum, ContDiffAt.laplacianWithin_add_nhdsWithin, orderedSub, ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF, fourierCoeff.add, HasFiniteFPowerSeriesAt.add, MeromorphicOn.min_divisor_le_divisor_add, Finset.weightedVSub_vadd_affineCombination, List.measurable_sum, AddEquiv.val_piAddUnits_symm_apply, MeasureTheory.stoppedProcess_eq', MeasureTheory.martingalePart_add_ae_eq, DFinsupp.mk_add, MeasureTheory.integral_add', CauSeq.coe_add, OnePoint.IsBoundedAt.add, ValueDistribution.logCounting_add_const, MeasureTheory.Integrable.add, Monovary.add_left, DiffContOnCl.add, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, ContinuousWithinAt.add, limsup_add_le, Finsupp.liftAddHom_singleAddHom, MeromorphicOn.negPart_divisor_add_le_max, MeasureTheory.martingalePart_eq_sum, HasFPowerSeriesWithinOnBall.add, RingEquiv.piCongrLeft'_symm_apply, ValueDistribution.characteristic_zero_mul_le, MeasureTheory.L1.setToL1_add_left, DFinsupp.liftAddHom_singleAddHom, Monovary.add_right, TorusIntegrable.add, eHolderNorm_add_le, MeasureTheory.StronglyAdapted.add, AddEquiv.piCongrRight_trans, Finsupp.lift_symm_apply, VectorField.lieBracket_add_right, ValueDistribution.logCounting_top_mul_le, MeasureTheory.integrable_add_iff_integrable_right, Matrix.head_add, UniformFun.toFun_add, ContinuousAlternatingMap.map_piecewise_add, measurableAdd₂, Fin.insertNth_add, StrictConcaveOn.add_concaveOn, Matrix.cons_add, EReal.le_limsup_add, ModularForm.coe_add, LinearMap.IsAdjointPair.add, RingEquiv.sumArrowEquivProdArrow_apply, MeasureTheory.ConvolutionExistsAt.distrib_add, MeasureTheory.withDensity_add_right, Finsupp.liftAddHom_apply_single, Sum.elim_add_add, Function.Odd.add, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, Filter.isBoundedUnder_ge_add, constAddHom_apply, MeasureTheory.eLpNorm_add_le, list_sum_apply, MeasureTheory.MemLp.toLp_add, DifferentiableAt.add_iff_right, ProbabilityTheory.Kernel.integral_integral_add'_comp, NumberField.mixedEmbedding.fundamentalCone.expMap_add, Matrix.sumElim_vecMul_fromRows, Matrix.cons_vecMul, Filter.ZeroAtFilter.add, Sigma.curry_add, Filter.EventuallyEq.add, Matrix.cons_vecMul_cons, HasFPowerSeriesWithinAt.add, DifferentiableOn.add, MeasureTheory.integrable_add_iff_integrable_left, FreeAbelianGroup.lift_add_apply, le_liminf_add, update_eq_sub_add_single, Matrix.diag_list_sum, Set.addCenter_pi, UniformOnFun.toFun_add, RingEquiv.piFinTwo_symm_apply, Set.indicator_union_add_inter, RCLike.wInner_add_left, MeasureTheory.eLpNorm'_add_le, ENNReal.lintegral_Lp_add_le_of_le_one, LinearGrowth.linearGrowthInf_add_le, StrictConcaveOn.add_const, UniformConvexOn.sub, Function.locallyFinsuppWithin.coe_add, ProbabilityTheory.IndepFun.add_hasPDF, Finsupp.liftAddHom_symm_apply_apply, SlashInvariantForm.coe_add, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, MeromorphicOn.negPart_divisor_add_le_add, MeasureTheory.DominatedFinMeasAdditive.add, ENNReal.liminf_add_of_left_tendsto_zero, Asymptotics.IsLittleO.right_isBigO_add', StrictConvexOn.add_const, ProbabilityTheory.IndepFun.integrable_exp_mul_add, WeakFEPair.f_modif_aux1, CompactlySupportedContinuousMap.coe_add, ContinuousOn.add, mdifferentiable_add_section, Set.indicator_compl_add_self, jacobi_cross, StrictConcaveOn.add, AddEquiv.val_neg_piAddUnits_symm_apply, Finsupp.liftAddHom_symm_apply, MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt, MeasureTheory.ConvolutionExists.distrib_add, MeasureTheory.UnifIntegrable.add, iteratedDerivWithin_add, MeasureTheory.integral_integral_add', ProbabilityTheory.aestronglyMeasurable_exp_mul_add, LocallyConstant.coe_add, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map', meromorphicOrderAt_add_eq_right_of_lt, fderivWithin_add, MeasureTheory.eLpNorm_add_le', DFinsupp.liftAddHom_comp_single, ValueDistribution.proximity_top_mul_le, Measurable.add_iff_left, MeasureTheory.Integrable.toL1_add, UniformFun.ofFun_add, TendstoUniformlyOn.add, ProbabilityTheory.IndepFun.mgf_add, MonovaryOn.add_left, isIsometricVAdd'', existsAddOfLe, Matrix.fromCols_mulVec_sumElim, FreeAbelianGroup.liftAddEquiv_apply_apply, fwdDiff_add, Memℓp.add, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, NormedAddGroupHom.coe_add, Matrix.piLinearEquiv_symm_apply, GroupSeminorm.coe_add, IsLocallyConstant.add, List.stronglyMeasurable_sum, map_comp_add_neg, ProbabilityTheory.Kernel.rnDeriv_add, EReal.liminf_add_gt_of_gt, UniformOnFun.ofFun_add, Real.circleAverage_add, ContMDiff.add_section, ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right, Asymptotics.IsLittleOTVS.add, curveIntegral_add, StrictConvexOn.add_convexOn, ENNReal.limsup_add_le, Continuous.add, LinearPMap.coe_vadd, ConvexOn.add, meromorphicOrderAt_add_of_top_right, Function.update_add, IsModuleTopology.instPi, ValueDistribution.characteristic_top_mul_eventually_le, ConvexOn.add_const, MeasureTheory.AEEqFun.mk_add_mk, Asymptotics.IsLittleO.add_isEquivalent, WittVector.ghostEquiv_coe, VectorField.lieBracketWithin_add_right, instContinuousAddForallOfIsTopologicalSemiring, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, derivWithin_add, EReal.limsup_add_bot_of_ne_top, RingEquiv.piCongrRight_symm, indicator_union_eventuallyEq, ConvexOn.exists_affine_le_of_lt, Differentiable.add, ZeroAtInftyContinuousMap.coe_add, RingEquiv.piCongrRight_trans, ConvexOn.real_sSup_of_nat_affine_eq, Matrix.vecMul_cons, ValueDistribution.characteristic_sum_top_eventuallyLE, Complex.logTaylor_succ, ProbabilityTheory.IndepFun.charFun_map_add_eq_mul, ConcaveOn.add_strictConcaveOn, MeasureTheory.Measure.rnDeriv_add', ProbabilityTheory.iIndepFun.indepFun_add_right, Matrix.mulVec_cons, continuousAdd, DifferentiableAt.add, RingEquiv.piOptionEquivProd_symm_apply, IsCauSeq.add, MeasureTheory.Measure.pi.isAddLeftInvariant, ProbabilityTheory.HasSubgaussianMGF_add_of_HasCondSubgaussianMGF, Ideal.Factors.piQuotientEquiv_mk, mdifferentiableOn_add_section, RingEquiv.piFinTwo_apply, Filter.EventuallyEq.add_right, DFinsupp.liftAddHom_symm_apply, LieModule.coe_chainTop', Matrix.det_updateRow_add, MeasureTheory.Pi.isAddLeftInvariant_volume, MulActionHom.coe_add, Matrix.fromCols_mulVec, ContinuousAlternatingMap.coe_add, MeasureTheory.condLExp_add_le, AddEquiv.piCongrRight_apply, IsPoly.add, RCLike.wInner_add_right, Matrix.coe_ofAddEquiv, RingEquiv.piUnique_apply, isAddLeftRegular_iff, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map, evalAddHom_apply, ContMDiffOn.add, MeasureTheory.StronglyMeasurable.add, ConvexOn.sSup_affine_eq, QuaternionAlgebra.coe_addEquivTuple, BoxIntegral.HasIntegral.add, HahnSeries.coeff_add', IsDedekindDomain.quotientEquivPiFactors_mk, Filter.EventuallyLE.add_le_add, ENNReal.limsup_add_of_left_tendsto_zero, CurveIntegrable.add, AntivaryOn.add_right, mulInvariantVectorField_add, LieModule.genWeightSpace_neg_add_chainBot, CircleIntegrable.add, EReal.limsup_add_le_of_le, AddEquiv.val_piAddUnits_apply, MeasureTheory.ConvolutionExists.add_distrib, BoxIntegral.Integrable.add, deriv_add, ConvexOn.real_sSup_affine_eq, MeasureTheory.Supermartingale.add, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, Filter.EventuallyEq.add_left, LieModule.genWeightSpace_add_chainTop, Measurable.add_iff_right, Asymptotics.IsLittleO.right_isTheta_add', EisensteinSeries.D2_mul, Set.indicator_add_eq_left, Matrix.piAddEquiv_apply, LinearGrowth.le_linearGrowthInf_add, AddCommute.pi, CuspForm.coe_add, addSemiconjBy_iff, NumberField.mixedEmbedding.logMap_mul, ConvexOn.univ_sSup_of_nat_affine_eq, ContMDiffAt.add, ValueDistribution.characteristic_mul_top_eventuallyLE, Set.indicator_add_eq_right, EReal.limsup_add_le, analyticOrderAt_add_of_ne, AddSemiconjBy.pi, QuaternionAlgebra.coe_symm_addEquivTuple, dotProduct_add, Rep.indResHomEquiv_symm_apply_hom, ProbabilityTheory.IndepFun.hasLaw_add, InnerProductSpace.HarmonicAt.add, MeasureTheory.AEStronglyMeasurable.add_iff_right, addInvariantVectorField_add, ValueDistribution.logCounting_mul_zero_le, ZeroHom.coe_add, Ideal.Factors.piQuotientEquiv_map, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀, ProbabilityTheory.IndepFun.mgf_add', VectorField.mpullbackWithin_add_apply, MeasureTheory.SignedMeasure.rnDeriv_add, Matrix.replicateCol_add, MultilinearMap.map_add_univ, MeasureTheory.stoppedValue_piecewise_const', MulEquiv.piMultiplicative_symm_apply, ProbabilityTheory.Kernel.iIndepFun.indepFun_add_mul₀, Polynomial.sum_add'
instDiv 📖	CompOp	121 math math: div_def, update_eq_div_mul_mulSingle, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right, ContMDiff.div₀, TendstoLocallyUniformlyOn.div₀, Function.Antiperiodic.div, ProbabilityTheory.iIndepFun.indepFun_div_right, DifferentiableAt.div, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div₀, Antivary.div_right, AntivaryOn.div_right₀, mulSingle_div, MeasureTheory.div_ae_eq_one, UniformOnFun.toFun_div, MonovaryOn.div_right₀, ContMDiffAt.div₀, HasStrictDerivAt.div, Meromorphic.div, UniformOnFun.ofFun_div, Function.const_div, summable_const_div_iff, Filter.EventuallyEq.div, Monovary.div_right₀, ProbabilityTheory.iIndepFun.indepFun_div_left, map_comp_div, ProbabilityTheory.iIndepFun.indepFun_div_left₀, Asymptotics.IsBigO.eventually_mul_div_cancel, TendstoLocallyUniformlyOn.div, MeasureTheory.AEStronglyMeasurable.div, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div, MeromorphicOn.div, hasSum_const_div_iff, AEMeasurable.div', ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right₀, measurableDiv, MeasureTheory.uniformIntegrable_average_real, Asymptotics.IsBigOWith.eventually_mul_div_cancel, Filter.Tendsto.div, AntivaryOn.div_right, EisensteinSeries.finGcdMap_div, UniformFun.ofFun_div, ContinuousOn.div, Set.mulIndicator_div', MeasureTheory.StronglyMeasurable.div, div_comp, ProbabilityTheory.iIndepFun.indepFun_div_div₀, Monovary.div_right, UniformFun.toFun_div, ProbabilityTheory.iCondIndepFun.indepFun_div_right, div_apply, Function.Periodic.div, HasDerivWithinAt.div, TendstoLocallyUniformly.div₀, AntivaryOn.div_left₀, ContDiffOn.div, ProbabilityTheory.iIndepFun.indepFun_div_div, Continuous.div, MonovaryOn.div_right, OneHom.coe_div, MeasureTheory.StronglyAdapted.div, ProbabilityTheory.iCondIndepFun.indepFun_div_left, Asymptotics.IsEquivalent.div, MonovaryOn.div_left₀, Set.mulIndicator_compl', ProbabilityTheory.iCondIndepFun.indepFun_div_div, Function.support_div', DifferentiableWithinAt.div, Filter.Germ.coe_div, DifferentiableOn.div, Fin.insertNth_div, Filter.Tendsto.uniformity_div, ContMDiffMap.coe_div, Fin.insertNth_div_same, MeasureTheory.lpNorm_div_natCast, Set.piecewise_div, Monovary.div_left₀, deriv_div, MeasureTheory.SimpleFunc.coe_div, Fintype.piFinset_div, Set.MapsTo.div, Asymptotics.isEquivalent_iff_tendsto_one, MeasureTheory.AEEqFun.mk_div, ProbabilityTheory.iIndepFun.indepFun_div_right₀, HasCompactSupport.div, Monovary.div_left, ContinuousAt.div, HasDerivAt.div, ContinuousMap.coe_div, Antivary.div_right₀, MeasureTheory.Adapted.div, Measurable.div', AntivaryOn.div_left, LocallyConstant.coe_div, MeromorphicAt.div, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left, derivWithin_div, measurableDiv₂, TendstoLocallyUniformly.div, Asymptotics.IsLittleO.eventually_mul_div_cancel, AnalyticAt.div, map_comp_div', ContMDiffWithinAt.div₀, UniformCauchySeqOn.div, Antivary.div_left₀, IsMulFreimanHom.div, TendstoUniformly.div, ContinuousWithinAt.div, MonovaryOn.div_left, IsLocallyConstant.div, ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left₀, TendstoUniformlyOnFilter.div, Function.update_div, MeasureTheory.AEEqFun.coeFn_div, Function.extend_div, Set.mulIndicator_diff', Antivary.div_left, Differentiable.div, TendstoUniformlyOn.div, Sum.elim_div_div, ContMDiffOn.div₀, MeasureTheory.one_le_div_ae
instInv 📖	CompOp	176 math math: continuousInv, monovaryOn_inv₀, MeasureTheory.AEStronglyMeasurable.inv, Antivary.inv_right, Function.mulSupport_inv, TendstoLocallyUniformly.inv, UniformCauchySeqOn.inv, Sum.elim_inv_inv, Sigma.uncurry_inv, TendstoLocallyUniformlyOn.inv₀, TendstoUniformly.inv, monovary_inv, Asymptotics.SuperpolynomialDecay.param_inv_mul, MeasureTheory.Measure.inv_rnDeriv', MeasureTheory.Measure.pi.isInvInvariant, monovary_inv_left, DiffContOnCl.inv, AntilipschitzWith.inv, AntivaryOn.inv_left₀, MonovaryOn.inv_right, Set.inv_pi, antivary_inv₀, MeromorphicAt.inv_iff, monovaryOn_inv, MeasureTheory.AEEqFun.inv_mk, antivaryOn_inv_left₀, ValueDistribution.proximity_inv, antivaryOn_inv_right, LocallyLipschitz.inv, antivary_inv, MeromorphicOn.divisor_inv, has_continuous_inv', UniformOnFun.ofFun_inv, monovary_inv_right₀, Antivary.inv_right₀, MeasureTheory.StronglyAdapted.inv, ExpGrowth.expGrowthInf_inv, ExpGrowth.expGrowthSup_inv, MeasureTheory.StronglyMeasurable.inv, monovaryOn_inv_right, AnalyticWithinAt.inv, Filter.EventuallyConst.inv, ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero, DifferentiableOn.inv, ValueDistribution.characteristic_sub_characteristic_inv_at_zero, MonovaryOn.inv_left₀, Antivary.inv_left₀, Filter.Tendsto.uniformity_inv_iff, HasCompactMulSupport.inv, meromorphicNFAt_inv, mulSingle_inv, LipschitzWith.inv, antivary_inv_right₀, Monovary.inv_right, CauSeq.coe_inv, Set.mulIndicator_inv', meromorphicOrderAt_inv, Function.update_inv, MonovaryOn.inv_right₀, Monovary.inv_left, measurableInv, MeasureTheory.Pi.isInvInvariant_volume, UniformContinuousOn.inv₀, ValueDistribution.characteristic_sub_characteristic_inv_le, MeromorphicOn.inv_iff, Filter.Tendsto.uniformity_inv, meromorphicTrailingCoeffAt_inv, DifferentiableAt.inv, Filter.Tendsto.conj_nhds_one, DifferentiableWithinAt.inv, meromorphicNFOn_inv, MeasureTheory.Measure.inv_rnDeriv, inv_comp, Antivary.inv, antivaryOn_inv₀, Monovary.inv_right₀, Antivary.inv₀, RegularWreathProduct.inv_left, MeromorphicOn.inv, ValueDistribution.characteristic_sub_characteristic_inv, Monovary.inv_left₀, ValueDistribution.isBigO_characteristic_sub_characteristic_inv, AnalyticOn.inv, lipschitzWith_inv_iff, deriv_inv'', antivary_inv_left, antivaryOn_inv, TendstoLocallyUniformlyOn.inv₀_of_disjoint, continuousOn_inv_iff, UniformContinuous.inv₀, antivaryOn_inv_left, MeasureTheory.withDensity_inv_same_le, Monovary.inv₀, Sigma.curry_inv, Filter.EventuallyEq.inv, derivWithin_inv', ProbabilityTheory.IdentDistrib.inv, HasDerivWithinAt.inv, TendstoUniformlyOnFilter.inv, MonovaryOn.inv₀, CauchySeq.inv, IsLocallyConstant.inv, ValueDistribution.proximity_zero_of_complexValued, OneHom.coe_inv, MeasureTheory.Measure.instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite, monovaryOn_inv_left₀, lipschitzOnWith_inv_iff, Monovary.inv, Filter.Germ.coe_inv, MeasureTheory.AEEqFun.coeFn_inv, Fintype.piFinset_inv, continuous_inv_iff, IsLocalMin.inv, TendstoLocallyUniformly.inv₀_of_disjoint, MeasureTheory.Measure.inv_rnDeriv_aux, Asymptotics.SuperpolynomialDecay.inv_param_mul, Filter.Tendsto.inv_tendsto_nhdsLT_zero, TendstoLocallyUniformlyOn.inv, TendstoLocallyUniformly.inv₀, Asymptotics.IsEquivalent.inv, LocallyConstant.coe_inv, Set.mulIndicator_diff, TendstoUniformlyOn.inv, Function.extend_inv, AntivaryOn.inv, MeasureTheory.Adapted.inv, map_comp_inv, Filter.Tendsto.inv_tendsto_nhdsGT_zero, ContinuousMap.coe_inv, monovary_inv₀, AntivaryOn.inv_right₀, IsMulFreimanHom.inv, continuousAt_inv_iff, UniformOnFun.toFun_inv, MeromorphicAt.inv, Meromorphic.inv, Filter.Tendsto.inv_tendsto_atTop, MonovaryOn.inv, UniformFun.toFun_inv, antilipschitzWith_inv_iff, LocallyLipschitzOn.inv, mulTSupport_inv, Function.const_inv, monovary_inv_left₀, Set.mulIndicator_compl, AntivaryOn.inv₀, monovary_inv_right, locallyLipschitz_inv_iff, AnalyticAt.inv, inv_def, MeromorphicNFAt.inv, Function.support_inv', ContMDiffMap.coe_inv, AntivaryOn.inv_right, MonovaryOn.inv_left, AntivaryOn.inv_left, antivaryOn_inv_right₀, Set.piecewise_inv, MeasureTheory.SimpleFunc.coe_inv, Differentiable.inv, ValueDistribution.logCounting_inv, inv_apply, Antivary.inv_left, antivary_inv_left₀, locallyLipschitzOn_inv_iff, monovaryOn_inv_right₀, LipschitzOnWith.inv, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, HasDerivAt.inv, Set.MapsTo.inv, antivary_inv_right, Filter.Tendsto.inv_tendsto_atBot, AnalyticOnNhd.inv, map_comp_mul_inv, UniformFun.ofFun_inv, monovaryOn_inv_left
instMul 📖	CompOp	538 math math: Finset.sup'_mul_le_mul_sup'_of_nonneg, ModularForm.coe_mul, RingEquiv.piCongrRight_apply, update_eq_div_mul_mulSingle, ModularForm.mul_slash_SL2, meromorphicNFOn_mul_iff_right_of_analyticOnNhd, ConvexOn.mul_concaveOn', HasMFDerivAt.mul, MeasureTheory.Adapted.mul, existsMulOfLe, Meromorphic.mul, Antivary.mul_left, ProbabilityTheory.IndepFun.mul_hasPDF', Real.iteratedDeriv_odd_cos, Function.Even.mul_odd, FDRep.char_tensor, ENNReal.le_liminf_mul, StrictMono.mul, ModularForm.mul_slash, ProbabilityTheory.condIndep_iff, MeasureTheory.Submartingale.sum_mul_sub', Filter.BoundedAtFilter.mul, DifferentiableAt.mul, ProbabilityTheory.iCondIndepFun.indepFun_mul_right, mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle, AddEquiv.piAdditive_apply, ValueDistribution.characteristic_mul_top_le, Asymptotics.SuperpolynomialDecay.param_inv_mul, Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow, MeasureTheory.Measure.rnDeriv_mul_rnDeriv', TendstoLocallyUniformlyOn.mul₀_of_isBoundedUnder, Measurable.mul_iff_right, MonovaryOn.mul_right, ValueDistribution.logCounting_zero_mul_le, MeasureTheory.MemLp.integrable_mul, MeromorphicAt.mul, ValueDistribution.proximity_zero_mul_le, CompactlySupportedContinuousMap.coe_mul, MDifferentiableWithinAt.mul, UniformCauchySeqOn.mul, MulEquiv.piMultiplicative_apply, MeasureTheory.AEEqFun.coeFn_mul, AddChar.coe_mul, MeasureTheory.StronglyMeasurable.mul_iff_left, List.periodic_prod, MonovaryOn.mul_right₀, mul_apply, meromorphicOrderAt_mul, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀, MulEquiv.piCongrRight_refl, MeasureTheory.Integrable.simpleFunc_mul', ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one, constMulHom_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul, analyticAt_iff_analytic_mul, HasStrictFDerivAt.mul', MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul, ContinuousMapZero.coe_mul, DirichletCharacter.LSeries_twist_vonMangoldt_eq, Algebra.TensorProduct.piRightHom_mul, ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun', ENNReal.limsup_mul_le, MeasureTheory.Submartingale.sum_upcrossingStrat_mul, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, MeasureTheory.lintegral_withDensity_eq_lintegral_mul, RingEquiv.piOptionEquivProd_apply, RingEquiv.piCongrLeft_symm_apply, BoundedContinuousFunction.coe_mul, RingEquiv.piCongrLeft'_symm, Filter.EventuallyEq.mul, RingEquiv.piCongrLeft'_apply, AntivaryOn.mul_left, Set.mulIndicator_mul_compl_eq_piecewise, MeasureTheory.Integrable.simpleFunc_mul, ProbabilityTheory.IndepFun.hasLaw_mul, ProbabilityTheory.iCondIndepFun.indepFun_mul_mul, MulEquiv.val_piUnits_symm_apply, HasFDerivWithinAt.mul, DifferentiableOn.mul, commute_iff, MvPowerSeries.rescale_mul, ProbabilityTheory.IndepFun.integral_comp_mul_comp, Matrix.diag_vecMulVec, ValueDistribution.logCounting_mul_zero_eventuallyLE, Matrix.hadamard_diagonal_eq_diagonal_iff, Matrix.diag_replicateCol_mul_replicateRow, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul₀, DirichletCharacter.mul_delta, Filter.EventuallyLE.mul_le_mul, MDifferentiableAt.mul, ValueDistribution.logCounting_mul_top_eventuallyLE, meromorphicOrderAt_mul_of_ne_zero, mulSingle_mul, Asymptotics.IsEquivalent.mul, ExpGrowth.expGrowthInf_mul_le, Function.support_mul', HasStrictDerivAt.mul, List.aemeasurable_prod, meromorphicNFAt_mul_iff_left, Tactic.ComputeAsymptotics.Majorized.mul, Matrix.piRingEquiv_apply, CauchySeq.mul, ProbabilityTheory.condIndepSets_singleton_iff, DifferentiableWithinAt.mul, isSemisimpleRing_iff_pi_matrix_divisionRing, CommGroup.equiv_prod_multiplicative_zmod_of_finite, MeasureTheory.Integrable.mul_of_top_right, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, MeasureTheory.lpNorm_mul_natCast, DihedralGroup.commProb_nil, Monotone.mul_strictMono, isIsometricSMul'', MeasureTheory.Submartingale.sum_mul_sub, Set.mulIndicator_mul', MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable, List.aestronglyMeasurable_prod, MvPowerSeries.HasEval.mul_right, MeasureTheory.StronglyMeasurable.mul_iff_right, DirichletCharacter.LSeriesSummable_mul, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map, Asymptotics.SuperpolynomialDecay.param_pow_mul, ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun, MeasureTheory.Measure.rnDeriv_mul_rnDeriv, ContMDiff.mul, Matrix.piRingEquiv_symm_apply, ProbabilityTheory.iIndepFun.indepFun_mul_right₀, MeasureTheory.withDensity_mul₀, RingEquiv.piCongrRight_refl, ProbabilityTheory.iIndepFun.indepFun_mul_right, TendstoLocallyUniformlyOn.mul, Matrix.vec_hadamard, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable, MonovaryOn.mul_left₀, isLeftRegular_iff, HasDerivWithinAt.mul, Asymptotics.IsBigO.eventually_mul_div_cancel, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', RingEquiv.piEquivPiSubtypeProd_symm_apply, Fin.insertNth_mul, TendstoUniformly.mul, single_mul_right, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul, Complex.iteratedDeriv_odd_sin, MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀, MeasureTheory.condExp_ofNat, ContMDiffOn.mul, fderiv_mul, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul, MeasureTheory.Measure.instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite, ProbabilityTheory.condIndepSet_iff, Asymptotics.isEquivalent_iff_exists_eq_mul, MulEquiv.arrowCongr_apply, DirichletCharacter.LSeries.mul_mu_eq_one, Function.Antiperiodic.mul, MeasureTheory.SimpleFunc.coe_mul, ConcaveOn.mul', lp.infty_coeFn_mul, IsLinearTopology.tendsto_mul_zero_of_left, Finset.mul_inf_le_inf_mul_of_nonneg, Monovary.mul_right₀, MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀, TendstoUniformlyOn.mul, MvPowerSeries.rescaleAlgHom_mul, fderiv_mul', AEMeasurable.mul_iff_right, Antivary.mul_right₀, ValueDistribution.proximity_mul_zero_le, ENNReal.liminf_mul_le, MulEquiv.val_inv_piUnits_apply, instIsLeftCancelMul, MeasureTheory.FinStronglyMeasurable.mul, iteratedDeriv_mul, MulEquiv.piCongrRight_symm, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf, Antitone.mul_monotone, RingEquiv.piEquivPiSubtypeProd_apply, Asymptotics.IsBigOWith.eventually_mul_div_cancel, OneHom.coe_mul, Poly.coe_mul, Filter.isBoundedUnder_le_mul_of_nonneg, TendstoUniformlyOnFilter.mul, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound, Set.mulIndicator_symmDiff, MvPowerSeries.HasSubst.mul_right, mul_bounded_of_bounded_of_bounded, meromorphicNFOn_mul_iff_left_of_analyticOnNhd, analyticOrderAt_mul, ContMDiffMap.coe_mul, MeasureTheory.MemLp.mul, MulEquiv.piCongrRight_trans, mulAutArrow_apply_apply, le_limsup_mul, ProbabilityTheory.iIndepFun.indepFun_mul_mul, AntivaryOn.mul_left₀, Filter.Tendsto.conj_nhds_one, LocallyConstant.coe_mul, MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le, Asymptotics.SuperpolynomialDecay.mul, Asymptotics.IsBigOWith.exists_eq_mul, HasCompactMulSupport.mul, MulActionHom.coe_mul, Set.MapsTo.mul, Finset.noncommProd_mul_distrib, ProbabilityTheory.covariance_eq_sub, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, MulHom.compLeft_apply, AddEquiv.piAdditive_symm_apply, SchwartzMap.smulLeftCLM_smulLeftCLM_apply, Module.rankAtStalk_tensorProduct, mulAutArrow_apply_symm_apply, ValueDistribution.logCounting_mul_top_le, ProbabilityTheory.condIndepSets_iff, MeasureTheory.Measure.instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite, Complex.ofReal_comp_mul, ValueDistribution.proximity_mul_top_le, DirichletCharacter.LSeriesSummable_twist_vonMangoldt, DirichletCharacter.convolution_twist_vonMangoldt, ValueDistribution.characteristic_mul_zero_eventuallyLE, ValueDistribution.characteristic_top_mul_le, ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top, MeasureTheory.Measure.pi.isMulRightInvariant, Asymptotics.isBigOWith_iff_exists_eq_mul, ValueDistribution.logCounting_top_mul_eventually_le, AntivaryOn.mul_right₀, instCanonicallyOrderedMulForall, MeasureTheory.StronglyAdapted.mul, measurableMul₂, ZeroAtInftyContinuousMap.coe_mul, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left, Monovary.mul_right, cuspFunction_mul, BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq, Set.mulIndicator_mul_eq_left, ExpGrowth.expGrowthSup_mul_le, RingEquiv.sumArrowEquivProdArrow_symm_apply, Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow, Real.iteratedDeriv_even_cos, HasMFDerivWithinAt.mul', MeasureTheory.AEStronglyMeasurable.mul_iff_left, EReal.le_limsup_mul, Complex.iteratedDeriv_even_cos, EReal.limsup_mul_le, MeasureTheory.StronglyMeasurable.mul, isNilpotent_of_finite_tfae, Asymptotics.superpolynomialDecay_mul_param_pow_iff, Continuous.mul, MonotoneOn.mul, EReal.le_liminf_mul, AEMeasurable.mul_iff_left, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, CommGroup.equiv_free_prod_prod_multiplicative_zmod, Filter.EventuallyLE.mul_nonneg, MeasureTheory.Measure.pi.isMulLeftInvariant, MulEquiv.funUnique_symm_apply, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf', MeasureTheory.Integrable.mul_of_top_left, HasFDerivAt.mul, MDifferentiable.mul, MeasureTheory.Integrable.const_mul', MulHom.coeFn_apply, RingEquiv.piUnique_symm_apply, ValueDistribution.characteristic_mul_zero_le, bddAbove_range_mul, MeasureTheory.withDensity_mul, MeasureTheory.Integrable.mul_const', ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, TwoUniqueProds.instForall, ProbabilityTheory.iIndepFun.indepFun_mul_left₀, MvPowerSeries.rescale_rescale, OrderMonoidHom.coe_mul, ValueDistribution.logCounting_zero_mul_eventually_le, Monovary.mul_left, UniqueProds.instForall, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀', Fintype.piFinset_mul, isRegular_iff, Filter.EventuallyEq.mul_right, Matrix.diagonal_hadamard, HasCompactSupport.mul_right, Asymptotics.IsEquivalent.exists_eq_mul, MeasureTheory.lintegral_withDensity_le_lintegral_mul, IsSemisimpleModule.exists_end_ringEquiv, MulEquiv.piUnique_apply, DirichletCharacter.mul_convolution_distrib, Tactic.ComputeAsymptotics.Majorized.mul_bounded, instPNatPowAssoc, Antivary.mul_left₀, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map', ENNReal.lintegral_mul_le_Lp_mul_Lq, isRightRegular_iff, EReal.liminf_mul_le, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀', MulHom.coe_mul, Function.extend_mul, mulIndicator_union_eventuallyEq, Asymptotics.isLittleO_iff_exists_eq_mul, Filter.isCoboundedUnder_ge_mul_of_nonneg, Antivary.mul_right, continuousMul', NumberField.mixedEmbedding.unitSMul_smul, RingEquiv.piCongrLeft_apply, Monotone.mul_antitone, iteratedDerivWithin_mul, Finset.sup_mul_le_mul_sup_of_nonneg, Function.Odd.mul_even, liminf_mul_le, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left₀, Matrix.invOf_diagonal_eq, AbsolutelyContinuousOnInterval.mul, Finset.noncommProd_mul_distrib_aux, Measurable.mul', IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, Asymptotics.IsBigO.exists_eq_mul, ValueDistribution.characteristic_zero_mul_eventually_le, MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀', ENNReal.essSup_mul_le, LSeries.mul_delta, MeasureTheory.AEStronglyMeasurable.mul_iff_right, Set.mulIndicator_mul_eq_right, OrderMonoidWithZeroHom.coe_mul, Filter.Tendsto.uniformity_mul, continuousMul, HasDerivAt.mul, MvPowerSeries.HasEval.mul_left, Real.iteratedDeriv_even_sin, DomMulAct.stabilizerMulEquiv_apply, PiTensorProduct.mul_tprod_tprod, ENNReal.limsup_mul_le', commProb_pi, commProb_function, Function.Even.mul_even, Filter.Tendsto.uniformity_mul_iff_right, HasCompactSupport.mul_left, LSeries.mul_delta_eq_smul_delta, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀', MulEquiv.piUnique_symm_apply, Memℓp.infty_mul, Matrix.diagonalInvertibleEquivInvertible_symm_apply, IsMulFreimanHom.mul, meromorphicAt_mul_iff_of_ne_zero, ContinuousAt.mul, TendstoLocallyUniformly.mul, Asymptotics.isBigO_iff_exists_eq_mul, ConcaveOn.mul, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, LSeries.delta_mul, ConvexOn.mul_concaveOn, ProbabilityTheory.iIndepFun.indepFun_mul_left, ExpGrowth.le_expGrowthSup_mul', Asymptotics.SuperpolynomialDecay.inv_param_mul, HasMFDerivWithinAt.mul, RingEquiv.piCongrLeft'_symm_apply, Complex.iteratedDeriv_odd_cos, ValueDistribution.characteristic_zero_mul_le, evalNonUnitalStarAlgHom_apply, Matrix.diagonal_hadamard_diagonal, AddChar.coe_add, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right, Int.subgroup_index_ne_zero_iff, UpperHalfPlane.mul_eq_zero_iff, Matrix.diagonalInvertibleEquivInvertible_apply, ExpGrowth.expGrowthInf_mul_le', ValueDistribution.logCounting_top_mul_le, Matrix.diagonal_hadamard_eq_diagonal_iff, qExpansion_mul, mulSingle_apply_commute, Function.FactorizedRational.extractFactor, RingEquiv.sumArrowEquivProdArrow_apply, conjneg_mul, mul_def, Set.mulIndicator_diff, IsCauSeq.mul, BumpCovering.exists_finset_toPOUFun_eventuallyEq, qExpansion_mul_coeff_zero, Antitone.mul, ProbabilityTheory.iCondIndepFun.indepFun_mul_left, ModularForm.cuspFunction_mul, IsLocallyConstant.mul, Complex.iteratedDeriv_even_sin, Monotone.mul, Asymptotics.superpolynomialDecay_param_mul_iff, ConvexOn.mul', Asymptotics.SuperpolynomialDecay.mul_param, Asymptotics.SuperpolynomialDecay.param_mul, NumberField.mixedEmbedding.fundamentalCone.expMap_add, single_mul_left, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀, MeasureTheory.lpNorm_natCast_mul, List.stronglyMeasurable_prod, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀, LSeries.delta_mul_eq_smul_delta, MulEquiv.funUnique_apply, AEMeasurable.mul', ProbabilityTheory.iIndepFun.indepFun_mul_mul₀, analyticOrderAt_mul_eq_top_of_left, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, Filter.EventuallyEq.mul_left, Function.HasTemperateGrowth.mul, list_prod_apply, RingEquiv.piFinTwo_symm_apply, MDifferentiableOn.mul, Real.iteratedDeriv_odd_sin, evalMulHom_apply, TendstoLocallyUniformlyOn.mul₀, StrictMono.mul_monotone, Sigma.curry_mul, Asymptotics.SuperpolynomialDecay.mul_param_pow, UniformOnFun.ofFun_mul, Filter.EventuallyLE.mul_le_mul', le_liminf_mul, AntivaryOn.mul_right, ContMDiffWithinAt.mul, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀, MulHom.single_apply, DirichletCharacter.delta_mul, Asymptotics.IsLittleO.eventually_mul_div_cancel, analyticOrderNatAt_mul, RegularWreathProduct.mul_def, ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀, Differentiable.mul, AnalyticAt.mul, UniformOnFun.toFun_mul, TendstoLocallyUniformly.mul₀, derivWithin_mul, HasStrictFDerivAt.mul, meromorphicNFAt_mul_iff_right, DirichletCharacter.convolution_mul_moebius, TendstoLocallyUniformly.mul₀_of_isBoundedUnder, ValueDistribution.proximity_top_mul_le, Set.center_pi, ConvexOn.mul, ProbabilityTheory.IndepFun.integrable_mul, ProbabilityTheory.indepFun_iff_integral_comp_mul, MeromorphicOn.mul, Set.mulIndicator_compl, Matrix.hadamard_diagonal, ConcaveOn.mul_convexOn, List.measurable_prod, Finsupp.coe_mul, ENNReal.le_limsup_mul, Function.const_mul, instIsRightCancelMul, Set.inter_indicator_one, MulEquiv.piCongrRight_apply, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, Function.update_mul, ProbabilityTheory.condIndepFun_iff, map_comp_mul, SchwartzMap.smulLeftCLM_compL_smulLeftCLM, ValueDistribution.characteristic_top_mul_eventually_le, HasFDerivWithinAt.mul', ContinuousOn.mul, WittVector.ghostEquiv_coe, deriv_mul, MulEquiv.val_piUnits_apply, analyticOrderAt_mul_eq_top_of_right, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, RingEquiv.piCongrRight_symm, fderivWithin_mul', semiconjBy_iff, Commute.pi, RegularWreathProduct.mul_left, Set.piecewise_mul, RingEquiv.piCongrRight_trans, ExpGrowth.le_expGrowthSup_mul, IsLinearTopology.tendsto_mul_zero_of_right, SlashInvariantForm.coe_mul, ProbabilityTheory.IndepFun.charFun_map_add_eq_mul, MeasureTheory.AEFinStronglyMeasurable.mul, cuspFunction_mul_zero, RingEquiv.piOptionEquivProd_symm_apply, UniformFun.toFun_mul, ContinuousMap.coe_mul, Function.Periodic.mul, Ideal.Factors.piQuotientEquiv_mk, MulChar.coeToFun_mul, Set.mulIndicator_union_mul_inter, Function.Odd.mul_odd, RingEquiv.piFinTwo_apply, Finset.inf'_mul_le_mul_inf'_of_nonneg, Monovary.mul_left₀, HasMFDerivAt.mul', measurableMul, MeromorphicAt.meromorphicTrailingCoeffAt_mul, PiTensorProduct.tprod_mul_tprod, MeromorphicOn.divisor_mul, MeasureTheory.AEStronglyMeasurable.mul, Asymptotics.IsLittleO.exists_eq_mul, ProbabilityTheory.IndepFun.mul_hasPDF, RingEquiv.piUnique_apply, ExpGrowth.le_expGrowthInf_mul, ContinuousWithinAt.mul, Sum.elim_mul_mul, ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero, IsDedekindDomain.quotientEquivPiFactors_mk, Filter.Tendsto.uniformity_mul_iff_left, MonovaryOn.mul_left, PiTensorProduct.smul_tprod_mul_smul_tprod, Asymptotics.superpolynomialDecay_param_pow_mul_iff, HasFDerivAt.mul', limsup_mul_le, ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr, Filter.EventuallyConst.mul, ModularForm.mul_coe, Filter.Germ.coe_mul, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, SemiconjBy.pi, mulHom_injective, Equiv.Perm.sigmaCongrRight_mul, Set.mulIndicator_self_mul_compl, MvPowerSeries.HasSubst.mul_left, NumberField.mixedEmbedding.logMap_mul, DihedralGroup.commProb_cons, ValueDistribution.characteristic_mul_top_eventuallyLE, NNReal.lintegral_mul_le_Lp_mul_Lq, Measurable.mul_iff_left, Sigma.uncurry_mul, fderivWithin_mul, UniformFun.ofFun_mul, ValueDistribution.logCounting_mul_zero_le, Ideal.Factors.piQuotientEquiv_map, MeasureTheory.Pi.isMulLeftInvariant_volume, instIsCancelMul, MulEquiv.val_inv_piUnits_symm_apply, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral, ContMDiffAt.mul, mulHom_apply, DihedralGroup.commProb_reciprocal, Set.mulIndicator_compl_mul_self, CauSeq.coe_mul, map_comp_mul_inv, MeasureTheory.AEEqFun.mk_mul_mk, MulEquiv.piMultiplicative_symm_apply, Asymptotics.superpolynomialDecay_mul_param_iff, single_mul, ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top, mul_comp
instNeg 📖	CompOp	384 math math: Finsupp.coe_neg, MeasureTheory.StronglyMeasurable.neg, Matrix.circulant_neg, locallyLipschitz_neg_iff, Real.iteratedDeriv_odd_cos, MeasureTheory.LocallyIntegrableOn.neg, HasFiniteFPowerSeriesAt.neg, ProbabilityTheory.covariance_neg_left, MeasureTheory.Measure.instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite, TestFunction.coe_neg, HahnSeries.SummableFamily.coe_neg, MeasureTheory.lpNorm_neg, differentiableWithinAt_neg_iff, Finset.affineCombination_sdiff_sub, AntilipschitzWith.neg, BoxIntegral.Integrable.neg, ProbabilityTheory.mgf_neg, has_continuous_neg', StrictConvexOn.neg, Matrix.vec_neg, MeasureTheory.tilted_neg_same', Filter.Tendsto.uniformity_neg, HasFPowerSeriesAt.neg, neg_strictConvexOn_iff, AntivaryOn.neg_left, MeasureTheory.lintegral_enorm_neg, BoundedContinuousFunction.coe_neg, IntervalIntegrable.neg, Matrix.neg_cons, Matrix.vecMul_neg, LipschitzOnWith.neg, DFinsupp.mk_neg, Matrix.neg_vecMul_neg, LocallyLipschitzOn.neg, birkhoffAverage_neg, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, CircleIntegrable.neg, curveIntegral_neg, UniformOnFun.toFun_neg, Meromorphic.neg, HasFDerivAtFilter.neg, Matrix.neg_mulVec_neg, ProbabilityTheory.HasGaussianLaw.neg, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, TemperedDistribution.smulLeftCLM_neg, AnalyticOn.neg, Asymptotics.IsLittleOTVS.neg_right, Antivary.neg, NumberField.mixedEmbedding.convexBodySum_neg_mem, ModularForm.coe_neg, analyticAt_neg, fderiv_neg, Antivary.neg_right, MeasureTheory.VectorMeasure.coe_neg, MeasureTheory.Integrable.neg, MeasureTheory.AEEqFun.coeFn_neg, Asymptotics.IsBigOTVS.neg_right, Sigma.curry_neg, HasMFDerivAt.neg, DifferentiableAt.neg, MeasureTheory.AEFinStronglyMeasurable.neg, Function.extend_neg, LSeries_deriv_eqOn, ProbabilityTheory.IndepFun.neg_left, cross_anticomm, ContinuousLinearMap.coe_neg', Matrix.blockDiagonal'_neg, monovaryOn_neg, Filter.EventuallyConst.neg, HasMFDerivWithinAt.neg, BoxIntegral.integral_neg, LieModule.genWeightSpaceChain_neg, hasMFDerivAt_neg, LSeries_neg, EReal.limsup_neg, iteratedFDerivWithin_neg_apply, TendstoUniformlyOn.neg, Matrix.neg_of, RCLike.wInner_neg_right, Fintype.piFinset_neg, LinearEquiv.coe_neg, MeasureTheory.LocallyIntegrable.neg, Function.const_neg, Function.Periodic.cuspFunction_neg, derivWithin.neg, iteratedDeriv_const_sub, deriv.neg, HasDerivAt.neg, TendstoLocallyUniformlyOn.neg, HasFDerivWithinAt.neg, neg_convexOn_iff, tsupport_neg, MeasureTheory.condExp_neg, Set.indicator_compl', locallyLipschitzOn_neg_iff, TendstoLocallyUniformly.neg, Filter.Tendsto.conj_nhds_zero, Antivary.neg_left, MeromorphicAt.neg_iff, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem', ProbabilityTheory.CondIndepFun.neg_right, Complex.iteratedDeriv_odd_sin, VectorField.mpullbackWithin_neg_apply, LieModuleHom.coe_neg, Matrix.blockDiagonal_neg, Asymptotics.IsLittleOTVS.neg_left, Function.HasTemperateGrowth.neg, conjneg_neg, MeasureTheory.eLpNorm'_neg, antivaryOn_neg_left, cuspFunction_neg, IsAddFreimanHom.neg, WithCStarModule.neg_apply, ProbabilityTheory.Kernel.HasSubgaussianMGF.neg, slope_neg_fun, DFinsupp.coe_neg, BoxIntegral.integralSum_neg, Asymptotics.isBigOTVS_neg_right, Set.indicator_neg', CuspForm.coe_neg, UnitAddTorus.mFourier_neg, AbsolutelyContinuousOnInterval.neg, HasCompactSupport.neg, ProbabilityTheory.Kernel.IndepFun.neg_left, ProbabilityTheory.covariance_neg_right, Real.iteratedDeriv_add_one_cos, EisensteinSeries.D2_inv, iteratedFDeriv_neg_apply, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, AnalyticWithinAt.neg, LinearGrowth.linearGrowthSup_inv, Monovary.neg_right, VectorField.mpullbackWithin_neg, IncidenceAlgebra.coe_neg, MeasureTheory.tilted_neg_same, MeasureTheory.hasFiniteIntegral_neg_iff, antivary_neg, AkraBazziRecurrence.GrowsPolynomially.neg, Set.piecewise_neg, neg_comp, CentroidHom.coe_neg, ProbabilityTheory.gaussianReal_neg, MeasureTheory.condExpL1_neg, monovary_neg, ConvexOn.neg, Set.indicator_diff', HasStrictFDerivAt.neg, MeasureTheory.setToFun_neg, neg_concaveOn_iff, NumberField.mixedEmbedding.convexBodySumFun_neg, HasFPowerSeriesOnBall.neg, lipschitzOnWith_neg_iff, LSeriesSummable.neg_iff, ContinuousMapZero.coe_neg, Differentiable.neg, Asymptotics.isBigOTVS_neg_left, monovaryOn_neg_right, Matrix.neg_mulVec, LieDerivation.coe_neg, Matrix.blockDiag'_neg, Sigma.uncurry_neg, MeasureTheory.MemLp.toLp_neg, analyticOrderAt_neg, ContinuousMap.coe_neg, MeasureTheory.StronglyAdapted.neg, UniformConcaveOn.neg, IsCauSeq.neg, IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq, neg_dotProduct, MeromorphicOn.neg, BoxIntegral.HasIntegral.neg, curveIntegralFun_neg, MeasureTheory.AEStronglyMeasurable.neg, MonovaryOn.neg, MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc, NormedAddGroupHom.coe_neg, iteratedDerivWithin_neg, IsPoly.neg, ProbabilityTheory.cgf_neg, ProbabilityTheory.HasSubgaussianMGF.neg, MeasureTheory.withDensityᵥ_neg, ContinuousLinearEquiv.coe_neg, Real.iteratedDeriv_even_cos, MeasureTheory.eLpNorm_neg, LSeries.term_neg_apply, HasDerivWithinAt.neg, MeasureTheory.integral_neg', MeasureTheory.AEEqFun.neg_mk, HasFiniteFPowerSeriesOnBall.neg, Complex.iteratedDeriv_even_cos, Filter.Germ.coe_neg, Function.support_neg, DifferentiableWithinAt.neg, monovaryOn_neg_left, ProbabilityTheory.IndepFun.neg_right, Filter.Tendsto.uniformity_neg_iff, LeftInvariantDerivation.coe_neg, Sum.elim_neg_neg, MeasureTheory.Pi.isNegInvariant_volume, Complex.iteratedDeriv_add_one_cos, differentiableOn_neg_iff, fderivWithin_neg, continuousNeg, NumberField.mixedEmbedding.convexBodyLT_neg_mem, UniformCauchySeqOn.neg, curveIntegrable_neg_iff, MeasureTheory.Martingale.neg, LocallyConstant.coe_neg, MeasureTheory.Submartingale.neg, MDifferentiableAt.neg, Asymptotics.isLittleOTVS_neg_right, MeasureTheory.IntegrableAtFilter.neg, LSeries.term_neg, DifferentiableOn.neg, ProbabilityTheory.Kernel.IndepFun.neg_right, LipschitzWith.neg, antivary_neg_left, Fintype.balance_neg, EReal.liminf_neg, ContMDiffMap.coe_neg, UniformFun.ofFun_neg, IsLocallyConstant.neg, mdifferentiableAt_neg, ProbabilityTheory.CondIndepFun.neg_left, MeromorphicOn.neg_iff, MulActionHom.coe_neg, MeasureTheory.SimpleFunc.coe_neg, SlashInvariantForm.coe_neg, measurableNeg, MeasureTheory.MemLp.neg, NumberField.mixedEmbedding.normAtPlace_neg, MeasureTheory.Supermartingale.neg, SchwartzMap.smulLeftCLM_neg, MeasureTheory.FinStronglyMeasurable.neg, Filter.BoundedAtFilter.neg, QuadraticMap.polar_neg, Filter.EventuallyEq.neg, deriv.neg', QuadraticMap.coeFn_neg, AnalyticAt.neg, antivaryOn_neg, LieModule.chainTop_neg, LieModule.chainBot_neg, UniformFun.toFun_neg, AffineMap.coe_neg, differentiableAt_neg_iff, Matrix.diag_neg, Real.iteratedDeriv_even_sin, MeromorphicAt.neg, Matrix.mulVec_neg, neg_dotProduct_neg, StrictConcaveOn.neg, qExpansion_neg, HahnSeries.coeff_neg', ConcaveOn.neg, LocallyLipschitz.neg, TendstoUniformlyOnFilter.neg, AkraBazziRecurrence.GrowsPolynomially.neg_iff, HasFPowerSeriesWithinOnBall.neg, UniformConvexOn.neg, MeasureTheory.Adapted.neg, ProbabilityTheory.variance_neg, Filter.ZeroAtFilter.neg, ProbabilityTheory.condVar_neg, AdicCompletion.val_neg, RCLike.wInner_neg_left, IsPreconnected.eq_or_eq_neg_of_sq_eq, Complex.iteratedDeriv_odd_cos, MeasureTheory.Measure.pi.isNegInvariant, continuousAt_neg_iff, MeasureTheory.integrable_neg_iff, IsCompactOperator.neg, Poly.coe_neg, MDifferentiableOn.neg, Complex.iteratedDeriv_even_sin, HasFPowerSeriesWithinAt.neg, VectorField.mpullback_neg_apply, LieAlgebra.mem_corootSpace', MonovaryOn.neg_right, VectorField.lieBracketWithin_swap, MeasureTheory.SignedMeasure.rnDeriv_neg, ZeroHom.coe_neg, Function.update_neg, MeasureTheory.Lp.coeFn_neg, Matrix.vecMulVec_neg, single_neg, AntivaryOn.neg_right, Real.iteratedDeriv_odd_sin, ContDiffMapSupportedIn.coe_neg, LieModule.chainBotCoeff_neg, MeasureTheory.memLp_neg_iff, antivaryOn_neg_right, CompactlySupportedContinuousMap.coe_neg, Matrix.neg_vecMul, birkhoffSum_neg, curveIntegralFun_symm, VectorField.mpullback_neg, MeasureTheory.UnifTight.neg, Matrix.neg_vecMulVec, CauchySeq.neg, VectorField.mlieBracket_swap, lp.coeFn_neg, Memℓp.neg_iff, map_comp_neg, neg_cross, Asymptotics.IsBigOTVS.neg_left, Complex.logDeriv_cos, FreeAbelianGroup.lift_neg_apply, Hamming.ofHamming_neg, ContinuousAlternatingMap.coe_neg, Function.Antiperiodic.funext, AntivaryOn.neg, ProbabilityTheory.IdentDistrib.neg, BoxIntegral.integrable_neg, LieAlgebra.mem_corootSpace, MeasureTheory.UnifIntegrable.neg, CauSeq.coe_neg, MeasureTheory.HasFiniteIntegral.neg, continuous_neg_iff, map_comp_add_neg, Matrix.tail_neg, Finset.centerMass_neg_left, Complex.ofReal_comp_neg, antilipschitzWith_neg_iff, monovary_neg_right, Finset.weightedVSub_sdiff_sub, iteratedDeriv_neg, CPolynomialAt.neg, MDifferentiable.neg, neg_strictConcaveOn_iff, Matrix.neg_empty, TorusIntegrable.neg, ContMDiffSection.coe_neg, isCauSeq_neg, Matrix.blockDiag_neg, Memℓp.neg, NumberField.mixedEmbedding.convexBodyLT'_neg_mem, FreeAbelianGroup.lift_neg, Real.logDeriv_cos, neg_apply, mfderiv_neg, LieModule.chainTopCoeff_neg, Affine.Simplex.excenterWeightsUnnorm_compl, HasStrictDerivAt.neg, VectorField.mlieBracketWithin_swap, Function.locallyFinsuppWithin.coe_neg, HasFDerivAt.neg, ZeroAtInftyContinuousMap.coe_neg, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, AnalyticOnNhd.neg, Hamming.toHamming_neg, translate_neg_right, Derivation.coe_neg, ContinuousAffineMap.coe_neg, Asymptotics.isLittleOTVS_neg_left, UniformOnFun.ofFun_neg, HasDerivAtFilter.neg, continuousOn_neg_iff, iteratedFDeriv_neg, LSeriesHasSum.neg, LieModule.genWeightSpace_neg_add_chainBot, neg_def, MeasureTheory.Integrable.toL1_neg, MonovaryOn.neg_left, antivary_neg_right, monovary_neg_left, CurveIntegrable.neg, dotProduct_neg, LieModule.Weight.coe_neg, lipschitzWith_neg_iff, Matrix.submatrix_neg, Set.MapsTo.neg, DiffContOnCl.neg, Finset.weightedVSubOfPoint_sdiff_sub, Monovary.neg_left, MeasureTheory.neg_llr, Monovary.neg, Set.neg_pi, MDifferentiableWithinAt.neg, TendstoUniformly.neg, Matrix.head_neg, differentiable_neg_iff, LinearGrowth.linearGrowthInf_neg, LSeriesSummable.neg
instOne 📖	CompOp	343 math math: Lagrange.interpolate_one, LSeries.convolution_one_eq_convolution_zeta, map_comp_one, exists_continuous_sum_one_of_isOpen_isCompact, RingHom.ker_evalRingHom, completelyRegularSpace_iff_isOpen, LSeries.abscissaOfAbsConv_one, exists_contMDiffMap_zero_one_of_isClosed, NumberField.mixedEmbedding.logMap_one, BumpCovering.eventuallyEq_one, Real.iteratedDeriv_odd_cos, MeasureTheory.charFun_eq_fourierIntegral', Function.one_le_const_of_one_le, Function.ExtendByOne.hom_apply, mulTSupport_eq_empty_iff, fderivWithin_one, HasCompactMulSupport.mulTSupport_extend_one_subset, UniformFun.ofFun_one, curry_mulSingle, BoundedContinuousFunction.coe_one, hasFDerivAt_one, UniformOnFun.toFun_one, Function.const_eq_one, ProbabilityTheory.Kernel.borelMarkovFromReal_apply', instZeroLEOneClass, SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one, Asymptotics.isLittleOTVS_one, Finset.prod_eq_prod_extend, PiLp.norm_toLp_one, ContDiffBump.eventuallyEq_one, DirichletCharacter.LSeries_modOne_eq, indicator_indepFun_pi_of_prod_bcf, Function.one_le_const, MeasureTheory.lintegral_indicator_one_le, Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, List.periodic_prod, Fin.insertNth_one_right, BoundedContinuousFunction.indicator_apply, Function.mulSupport_one_sub', SimpleGraph.incMatrix_apply_mul_incMatrix_apply, MeasureTheory.charFun_eq_fourierIntegral, MeasureTheory.withDensity_one, MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul, tprod_extend_one, Matrix.blockDiag_one, Set.mulIndicator_preimage, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, Set.image_mulSingle_Icc_right, conjneg_one, differentiableWithinAt_one, HasCompactMulSupport.mulTSupport_extend_one, Set.image_mulSingle_uIcc_left, Finset.prod_indicator_biUnion_finset_sub_indicator, SlashInvariantForm.one_coe_eq_one, Matrix.diagonal_one', Function.mulSupport_one_add', MeasureTheory.div_ae_eq_one, MeasureTheory.Measure.rnDeriv_eq_one_iff_eq, Function.mulSupport_fun_curry, exists_continuous_zero_one_of_isClosed, IsLocallyConstant.one, Set.image_mulSingle_Ioo_right, Matrix.blockDiagonal'_one, Function.MulExact.comp_eq_one, Matrix.hadamard_of_one, Filter.Germ.coe_one, mulVec_one_of_mem_doublyStochastic, List.aemeasurable_prod, PiLp.nnnorm_toLp_one, Sum.one_le_elim_iff, Function.update_one, one_apply, MvPolynomial.expand_zero, MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet, summable_const_div_iff, List.aestronglyMeasurable_prod, mulSingle_one, Matrix.vandermonde_eq_projVandermonde, ValueDistribution.isBigO_characteristic_sub_characteristic_shift, Function.FactorizedRational.mulSupport, one_comp, PowerSeries.mk_one_pow_eq_mk_choose_add, MeasureTheory.Measure.dirac_apply', differentiableOn_one, Real.LogDeriv_exp, fderiv_one, UniformOnFun.one_apply, Function.const_le_one_of_le_one, PiTensorProduct.one_def, hasDerivWithinAt_one, Real.one_div_one_sub_hasFPowerSeriesOnBall_zero, ArithmeticFunction.LSeries_zeta_eq, Complex.iteratedDeriv_odd_sin, Set.smul_indicator_one_apply, hasDerivAtFilter_one, exists_bounded_zero_one_of_closed, RegularWreathProduct.left_inl, Height.logHeight_one, Matrix.of_one_hadamard, exists_continuous_one_zero_of_isCompact, Complex.logDeriv_exp, MvPowerSeries.rescaleAlgHom_one, MeasureTheory.stronglyMeasurable_one, hasSum_const_div_iff, Matrix.one_vecMul, Function.const_le_one, Set.image_mulSingle_Ioo_left, Set.mulIndicator_ae_eq_one, MeasureTheory.integral_indicator_one, ArithmeticFunction.convolution_vonMangoldt_const_one, Equiv.Perm.sigmaCongrRight_one, Function.mulSupport_add_one', Function.one_lt_const, RCLike.wInner_one_eq_inner, SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one, MulActionHom.coe_one, Asymptotics.isLittleO_id_one, ModularForm.one_coe_eq_one, Set.eqOn_mulIndicator', Set.image_mulSingle_Icc_left, HasCompactMulSupport.one, hasFDerivWithinAt_one, Matrix.blockDiag'_one, Matrix.one_vecMulVec, exists_continuous_zero_one_of_isCompact', MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq, one_memℓp_infty, MeasureTheory.lintegral_indicator_one₀, Module.Basis.coe_singleton, MvPolynomial.weightedTotalDegree_one, Sum.elim_le_one_iff, one_le_mulSingle, indicator_indepFun_pi_of_bcf, UniformFun.toFun_one, continuous_one, Function.comp_eq_one_iff, MeasureTheory.tendsto_sum_indicator_atTop_iff', ProbabilityTheory.Kernel.rnDerivAux_le_one, MeasureTheory.Filtration.filtrationOfSet_eq_natural, Sum.elim_one_one, indicator_indepFun_process_of_bcf, Matrix.hadamard_one_eq_one_iff, HasCompactMulSupport.extend_one, contMDiffWithinAt_one, HasCompactMulSupport.eq_one_or_finiteDimensional, hasProd_one_iff_of_one_le, Matrix.one_hadamard_eq_one_iff, SmoothBumpCovering.eventuallyEq_one, mem_parallelepiped_iff, DirichletCharacter.modOne_eq_one, mulSingle_eq_one_iff, Function.disjoint_mulSupport_iff, Set.preimage_one, Function.mulSupport_extend_one_subset, IsOpen.measure_eq_biSup_integral_continuous, contMDiff_one, Sigma.curry_one, Real.iteratedDeriv_even_cos, LSeries_one_eq_riemannZeta, ValueDistribution.isBigO_characteristic_sub_characteristic_inv, Set.image_mulSingle_uIcc_right, contMDiffAt_one, Complex.iteratedDeriv_even_cos, AddChar.coe_zero, QuadraticForm.equivalent_sum_squares, MeasureTheory.pdf.IsUniform.pdf_eq, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', Function.extend_one, Sigma.uncurry_mulSingle_mulSingle, conjneg_eq_one, Sum.elim_mulSingle_one, Set.range_one, Set.indicator_pi_one_apply, cfc_one, ArithmeticFunction.LSeries_vonMangoldt_eq, mulSingle_le_one, MvPolynomial.weightedHomogeneousSubmodule_one, Matrix.vecMulVec_one, OneHom.coe_mulSingle, Real.logDeriv_exp, Set.indicator_one_preimage, hasCompactMulSupport_iff_eventuallyEq, LocallyConstant.coe_one, derivWithin_one, CompletelyRegularSpace.completely_regular, Function.mulSupport_disjoint_iff, measurable_one, lp.infty_coeFn_one, CauSeq.coe_one, exists_continuous_zero_one_of_isCompact, MeasureTheory.diracProba_toMeasure_apply', Algebra.TensorProduct.piRightHom_one, ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul, OneHom.mulSingle_apply, LSeriesSummable_one_iff, ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_indicator_mul_lintegral, Set.mulIndicator_eq_one', Set.image_mulSingle_Ico_left, PiTensorProduct.one_mul, comp_one, LSeries_one_mul_Lseries_moebius, deriv_one, MeasureTheory.upcrossingsBefore_eq_sum, LSeries.one_convolution_eq_zeta_convolution, ContinuousMonoidHom.coe_one, Function.const_one, LSeries_delta, RCLike.wInner_one_const_right, Matrix.invOf_diagonal_eq, MeasureTheory.lpNorm_one, hasDerivAt_one, Complex.LogDeriv_exp, one_vecMul_of_mem_doublyStochastic, PiTensorProduct.mul_one, one_mono, ValueDistribution.abs_characteristic_sub_characteristic_shift_eqO, ProbabilityTheory.Kernel.withDensity_one, LSeriesHasSum_one, Matrix.mem_colStochastic, hasStrictFDerivAt_one, Real.iteratedDeriv_even_sin, exists_smooth_zero_one_of_isClosed, one_def, MeasureTheory.ae_mem_limsup_atTop_iff, SmoothBumpCovering.eventuallyEq_one', Set.image_mulSingle_Ioc_right, one_anti, Matrix.diagonalInvertibleEquivInvertible_symm_apply, differentiable_one, indicator_indepFun_of_bcf, NumberField.mixedEmbedding.logMap_real, mem_doublyStochastic, BumpCovering.eventuallyEq_one', Complex.iteratedDeriv_odd_cos, Matrix.diag_one, exists_continuousMap_one_of_isCompact_subset_isOpen, Matrix.diagonalInvertibleEquivInvertible_apply, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, hasStrictDerivAt_one, ProbabilityTheory.Kernel.IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral, SmoothBumpFunction.eventuallyEq_one_of_dist_lt, MeasureTheory.Measure.dirac_apply, MeasureTheory.lintegral_indicator_one, Option.card_toFinset, Function.support_one, MeasureTheory.diracProba_toMeasure_apply, Complex.iteratedDeriv_even_sin, RCLike.wInner_one_const_left, ContDiffBump.eventuallyEq_one_of_mem_ball, IsCompact.measure_eq_biInf_integral_hasCompactSupport, MeasureTheory.Measure.rnDeriv_restrict_self, ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log, OrderMonoidHom.coe_one, Function.mulSupport_curry, List.stronglyMeasurable_prod, Function.mulSupport_extend_one, ModularForm.is_invariant_one', list_prod_apply, RegularWreathProduct.one_left, RCLike.wInner_one_eq_sum, Set.indicator_eq_zero_iff_notMem, Real.iteratedDeriv_odd_sin, Set.mulIndicator_one_preimage, Sum.elim_one_mulSingle, Set.image_mulSingle_Ico_right, Function.mulSupport_eq_empty_iff, Sigma.uncurry_one, indicator_indepFun_process_of_prod_bcf, MeasureTheory.Measure.le_dirac_apply, Finset.prod_indicator_biUnion_sub_indicator, ContMDiff.extend_one, Set.mulIndicator_one', Set.mulIndicator_empty', completelyRegularSpace_iff, AffineBasis.coe_coord_of_subsingleton_eq_one, ContinuousMap.coe_one, Set.piecewise_eq_mulIndicator, HasCompactMulSupport.continuous_extend_one, uncurry_mulSingle_mulSingle, MeasureTheory.lpNorm_one', ContMDiffMap.coe_one, Matrix.mem_rowStochastic, Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero, List.measurable_prod, OrthonormalBasis.coe_singleton, Module.Basis.orientation_neg_single, ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj, differentiableAt_one, MvPowerSeries.rescale_one, exists_tsupport_one_of_isOpen_isClosed, Set.inter_indicator_one, MeasureTheory.withDensity_indicator_one, ProbabilityTheory.Kernel.rnDeriv_self, multipliable_extend_one, contMDiffOn_one, BumpCovering.le_one', MeasureTheory.SimpleFunc.coe_one, exists_continuous_add_one_of_isCompact_nnreal, SmoothBumpFunction.eventuallyEq_one, Function.mulSupport_one, Module.rankAtStalk_self, AddChar.coe_eq_one, mem_finsuppAffineCoords_iff_linearCombination, SimpleGraph.incMatrix_apply, Real.pi_rpow_zero, LocallyConstant.coe_charFn, mulTSupport_one, Sigma.curry_mulSingle, MeasureTheory.Measure.rnDeriv_le_one_of_le, PowerSeries.mk_one_mul_one_sub_eq_one, AddChar.coe_one, Matrix.mulVec_one, one_dotProduct, ArithmeticFunction.const_one_eq_zeta, dotProduct_one, Set.indicator_prod_one, notMem_mulTSupport_iff_eventuallyEq, Function.const_lt_one, ModularForm.is_invariant_one, MeasureTheory.aestronglyMeasurable_one, Set.image_mulSingle_Ioc_left, Matrix.one_vecMul_of_mem_colStochastic, RCLike.wInner_cWeight_eq_smul_wInner_one, one_dotProduct_one, ProbabilityTheory.Kernel.swap_apply', RCLike.inner_eq_wInner_one, hasProd_extend_one, Matrix.blockDiagonal_one, Height.mulHeight_one, CompletelyRegularSpace.completely_regular_isOpen, normOneClass, Set.indicator_eq_one_iff_mem, MeasureTheory.Measure.rnDeriv_le_one_iff_le, MeasureTheory.one_le_div_ae, ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mul, MeasureTheory.AEEqFun.coeFn_one, MvPolynomial.expand_zero_apply, hasFDerivAtFilter_one, ContinuousMap.exists_mul_le_one_eqOn_ge, Matrix.one_vecMul_of_mem_rowStochastic, SeminormedGroup.tendstoUniformlyOn_one
instPow 📖	CompOp	161 math math: Real.iteratedDeriv_odd_cos, Asymptotics.IsEquivalent.zpow, Function.FactorizedRational.divisor, MeasureTheory.SimpleFunc.coe_zpow, MvPolynomial.eval₂_expand, HasStrictDerivAt.pow, HasStrictDerivAt.pow', map_comp_pow, ValueDistribution.logCounting_pow_top, Matrix.diagonal_pow, MonovaryOn.pow_right, ValueDistribution.proximity_pow_zero, MeromorphicOn.divisor_pow, AnalyticOn.pow, MDifferentiableAt.pow, Differentiable.pow, HasDerivAt.pow, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, Monovary.pow_right₀, Asymptotics.SuperpolynomialDecay.param_pow_mul, mulSingle_pow, Function.FactorizedRational.mulSupport, Meromorphic.zpow, Function.FactorizedRational.meromorphicOrderAt_eq, analyticOrderAt_centeredMonomial, Height.mulHeight_pow, deriv_pow, Function.FactorizedRational.finprod_eq_fun, Monovary.pow_left₀, MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, MonovaryOn.pow_right₀, Complex.iteratedDeriv_odd_sin, fderiv_pow', MvPolynomial.aeval_expand, pow_comp, mulSingle_zpow, MonovaryOn.pow_left, AnalyticOn.zpow_nonneg, MeasureTheory.SimpleFunc.coe_pow, NumberField.mixedEmbedding.fundamentalCone.expMap_smul, AddChar.coe_pow, Function.FactorizedRational.meromorphicNFOn_univ, CFC.rpow_eq_rpow_pi, instIsReducedForall, Filter.EventuallyEq.pow_const, MvPowerSeries.HasEval.pow, lp.infty_coeFn_pow, Function.FactorizedRational.analyticAt, MeromorphicOn.divisor_zpow, ContMDiffMap.coe_pow, Function.HasTemperateGrowth.pow, ValueDistribution.characteristic_pow_zero, Antivary.pow_left, Real.iteratedDeriv_even_cos, ProbabilityTheory.iteratedDeriv_mgf_zero, Complex.iteratedDeriv_even_cos, Asymptotics.IsEquivalent.pow, Asymptotics.superpolynomialDecay_mul_param_pow_iff, Tactic.ComputeAsymptotics.Majorized.self, Meromorphic.pow, AntivaryOn.pow_left₀, MeromorphicAt.pow, DifferentiableWithinAt.pow, MeromorphicOn.zpow, MeasureTheory.AEStronglyMeasurable.pow, HasDerivWithinAt.pow', pow_apply, Antivary.pow_right₀, AnalyticWithinAt.pow, AnalyticOn.zpow, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, instPNatPowAssoc, AnalyticOnNhd.zpow, ValueDistribution.characteristic_pow_top, Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt, Complex.ofReal_comp_pow, AntivaryOn.pow_right₀, CauSeq.coe_pow, ContinuousMap.coe_zpow, HasFDerivWithinAt.pow', CFC.nnrpow_eq_nnrpow_pi, MeasureTheory.StronglyMeasurable.pow, ProbabilityTheory.moment_def, Function.const_pow, DifferentiableOn.pow, AnalyticOnNhd.zpow_nonneg, Real.iteratedDeriv_even_sin, AnalyticWithinAt.zpow_nonneg, AnalyticAt.zpow_nonneg, meromorphicOrderAt_pow, MeromorphicOn.extract_zeros_poles, Matrix.blockDiagonal_pow, MvPolynomial.aeval_comp_expand, AnalyticWithinAt.zpow, prod_indicator_const, Complex.iteratedDeriv_odd_cos, HasFDerivAt.pow', HasStrictFDerivAt.pow', ValueDistribution.proximity_pow_top, ValueDistribution.logCounting_pow_zero, Function.FactorizedRational.extractFactor, HasDerivWithinAt.pow, Complex.iteratedDeriv_even_sin, MeromorphicAt.zpow, Monovary.pow_right, MeasureTheory.AEEqFun.mk_zpow, prod_indicator_const_apply, MeromorphicOn.pow, PiTensorProduct.mapL_pow, meromorphicOrderAt_zpow, Real.iteratedDeriv_odd_sin, HasDerivAt.pow', MeasureTheory.AEEqFun.coeFn_zpow, Asymptotics.SuperpolynomialDecay.mul_param_pow, MvPolynomial.coe_expand, MonovaryOn.pow_left₀, analyticOrderNatAt_pow, MeasureTheory.AEEqFun.coeFn_pow, Memℓp.infty_pow, Monovary.pow_left, Antivary.pow_left₀, fderivWithin_pow, DifferentiableAt.pow, AnalyticAt.pow, deriv_pow', AnalyticOnNhd.pow, Asymptotics.IsEquivalent.rpow, MvPolynomial.eval_expand, AddChar.coe_nsmul, Asymptotics.IsBigO.pow_of_le_right, ContinuousMap.coe_pow, Real.pi_rpow_zero, BoundedContinuousFunction.coe_npowRec, MDifferentiableWithinAt.pow, PiTensorProduct.map_pow, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational_off_support, MeromorphicAt.meromorphicTrailingCoeffAt_zpow, derivWithin_pow, AntivaryOn.pow_left, Filter.Germ.coe_pow, BoundedContinuousFunction.coe_pow, Asymptotics.superpolynomialDecay_param_pow_mul_iff, instNatPowAssoc, Height.logHeight_pow, MeromorphicAt.meromorphicTrailingCoeffAt_pow, AnalyticAt.zpow, Function.support_pow', MDifferentiableOn.pow, map_comp_zpow, Antivary.pow_right, pow_def, MeasureTheory.AEEqFun.mk_pow, Function.FactorizedRational.meromorphicNFOn, map_comp_zpow', derivWithin_pow', MvPolynomial.eval₂Hom_comp_expand, AntivaryOn.pow_right, MDifferentiable.pow, cfcUnits_zpow, Matrix.blockDiagonal'_pow, fderivWithin_pow'
instSMul 📖	CompOp	160 math math: smulCommClass', smul_comp, MonovaryOn.nsmul_left, image_update_openSegment, MulActionHom.coe_smul, Antivary.nsmul_right, Filter.smul_tendsto_smul_iff₀, Memℓp.const_smul, VectorField.mpullbackWithin_smul, instMeasurableConstSMul, Bornology.isVonNBounded_pi_iff, AdicCompletion.val_smul, addInvariantVectorField_smul, instPosSMulStrictMono, convex_pi, Submodule.quotientPi_aux.map_smul, VectorField.mlieBracketWithin_const_smul_right, le_egauge_pi, hammingDist_smul, extremePoints_pi, PiLp.isBoundedSMulSeminormedAddCommGroupToPi, DirectSum.mk_smul, Matrix.smul_empty, isCentralScalar, LinearMap.coe_smul, faithfulSMul_at, MeasureTheory.StronglyMeasurable.const_nsmul, CStarMatrix.inner_toCLM_conjTranspose_left, egauge_univ_pi, Hamming.ofHamming_smul, Function.update_smul, isScalarTower', ContMDiffMap.coe_nsmul, hammingDist_smul_le_hammingDist, Set.smul_set_pi, IsMIntegralCurveOn.comp_mul, ContinuousMultilinearMap.range_toUniformOnFun, ZeroHom.coe_smul, PiLp.instNormSMulClass, Filter.Germ.coe_nsmul, RCLike.mul_wInner_left, instIsIsometricSMulForall, VectorField.mpullback_smul_apply, Set.smul_set_pi_of_surjective, MultilinearMap.dfinsuppFamily_smul, ContMDiffSection.coe_smul, Asymptotics.IsLittleOTVS.pi, DomMulAct.instSMulCommClassForall_1, ContinuousMultilinearMap.hasBasis_nhds_zero, egauge_pi, VectorField.mlieBracketWithin_const_smul_left, IsDivSequence.smul, MultilinearMap.map_update_smul_left, instProperConstSMulForall, instPosSMulReflectLE, single_smul, map_comp_zsmul', ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, RCLike.wInner_smul_right, map_comp_nsmul, ContinuousMap.coe_nsmul, MeasureTheory.Adapted.smul, Hamming.toHamming_smul, RCLike.wInner_smul_left, DFinsupp.coe_smul, instSMulPosReflectLT, VectorField.mpullbackWithin_smul_apply, instSMulPosStrictMono, instContinuousSMulForall, AntivaryOn.nsmul_left, ContinuousMap.coe_zsmul, WithCStarModule.pi_inner, CStarMatrix.mul_entry_mul_eq_inner_toCLM, Set.piecewise_smul, Asymptotics.isBigOTVS_pi, instIsBoundedSMul, PiLp.smul_apply, PiLp.normSMulClassSeminormedAddCommGroupToPi, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, WithCStarModule.inner_single_right, smul_pi, MeasureTheory.StronglyAdapted.smul, AddMonoidHom.coe_smul, Matrix.blockDiag'_smul, Set.smul_set_pi_of_isUnit, IsEllDivSequence.smul, instPosSMulMono, lp.coeFn_smul, evalMulActionHom_apply, isSMulRegular_iff, measurableSMul, hammingNorm_smul_le_hammingNorm, Monovary.nsmul_left, isScalarTower, isMIntegralCurveAt_comp_mul_ne_zero, VectorField.mlieBracket_const_smul_left, instNormSMulClass, IsMIntegralCurve.comp_mul, DomMulAct.instSMulCommClassForall, map_comp_zsmul, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis, MultilinearMap.piFamily_smul, openSegment_subset, MonovaryOn.nsmul_right, mapsTo_tangentConeAt_pi, Matrix.smul_cons, VectorField.mpullback_smul, single_zsmul, Set.smul_set_univ_pi, instSMulPosMono, smul_univ_pi, Matrix.smul_mat_cons, isMIntegralCurveOn_comp_mul_ne_zero, BoundedContinuousFunction.coe_nsmul, WithCStarModule.inner_single_left, IsEllSequence.smul, hammingNorm_smul, single_nsmul, IsUnit.smul_tendsto_smul_iff, Function.Antiperiodic.smul, faithfulSMul, IsMIntegralCurveAt.comp_mul_ne_zero, ContinuousMultilinearMap.toUniformOnFun_toFun, Filter.smul_tendsto_smul_iff, image_update_segment, smul_pi₀, smulCommClass, instStarModuleForall, Antivary.nsmul_left, segment_subset, AddMonoid.End.coe_smul, instSMulPosReflectLE, Function.Periodic.smul, MeasureTheory.AEStronglyMeasurable.const_nsmul, mulInvariantVectorField_smul, smul_def, IsModuleTopology.instPi, starConvex_pi, Monovary.nsmul_right, instContinuousConstSMulForall, WithCStarModule.smul_apply, Set.smul_set_pi₀', IsSMulRegular.pi, ContinuousMultilinearMap.isUniformInducing_toUniformOnFun, Filter.EventuallyEq.const_smul, isMIntegralCurve_comp_mul_ne_zero, PiLp.instIsBoundedSMul, AntivaryOn.nsmul_right, Asymptotics.isLittleOTVS_pi, DFinsupp.mk_smul, Asymptotics.IsBigOTVS.pi, Matrix.blockDiagonal'_smul, Set.smul_set_pi₀, egauge_pi', noZeroSMulDivisors, CStarMatrix.inner_toCLM_conjTranspose_right, Function.smul_const, smul_pi_subset, VectorField.mlieBracket_const_smul_right, smul_apply
instStarForall 📖	CompOp	81 math math: ContinuousMapZero.coe_star, lp.coeFn_star, instTrivialStarForall, star_mulSingle, dotProduct_star_self_eq_zero, Matrix.posDef_iff_dotProduct_mulVec, Matrix.IsHermitian.eigenvalues_eq, star_dotProduct_toMatrix₂_mulVec, Matrix.star_vec, star_single, Memℓp.star_mem, Matrix.dotProduct_star_self_pos_iff, Matrix.conjTranspose_eq_diagonal, Matrix.posSemidef_vecMulVec_self_star, Matrix.star_dotProduct, single_star, CompactlySupportedContinuousMap.coe_star, MeasureTheory.MemLp.star, Matrix.dotProduct_star, Matrix.star_dotProduct_star, Matrix.star_vec_dotProduct_vec, MeasureTheory.AEStronglyMeasurable.star, MeasureTheory.SimpleFunc.coe_star, Matrix.star_vecMul, Matrix.Fin.conjTranspose_circulant, dotProduct_star_self_nonneg, star_finsuppProd, MeasureTheory.eLpNorm_star, Matrix.conjTranspose_replicateRow, Matrix.schur_complement_eq₂₂, LinearMap.toMatrix_innerₛₗ_apply, Matrix.PosSemidef.toLinearMap₂'_zero_iff, instContinuousStarForall, Filter.EventuallyEq.star, Function.star_sumElim, apply_eq_star_dotProduct_toMatrix₂_mulVec, Matrix.diagonal_conjTranspose, Matrix.posSemidef_vecMulVec_star_self, Matrix.schur_complement_eq₁₁, EuclideanSpace.inner_eq_star_dotProduct, star_apply, Memℓp.star_iff, dotProduct_self_star_nonneg, InnerProductSpace.toMatrix_rankOne, Matrix.PosSemidef.dotProduct_mulVec_nonneg, Matrix.mulVec_conjTranspose, Matrix.posSemidef_iff_eq_sum_vecMulVec, Matrix.vecMul_conjTranspose, star_def, MeasureTheory.AEEqFun.coeFn_star, Matrix.star_dotProduct_gram_mulVec, toMatrix_innerSL_apply, Matrix.PosSemidef.re_dotProduct_nonneg, Matrix.posSemidef_iff_dotProduct_mulVec, Matrix.PosSemidef.dotProduct_mulVec_zero_iff, Function.update_star, ContinuousMap.coe_star, BoundedContinuousFunction.coe_star, evalNonUnitalStarAlgHom_apply, Matrix.updateCol_conjTranspose, Matrix.conjTranspose_vecMulVec, EuclideanSpace.inner_toLp_toLp, dotProduct_self_star_eq_zero, star_finsuppSum, instStarModuleForall, Matrix.updateRow_conjTranspose, summable_star_iff', evalStarAlgHom_apply, isSelfAdjoint, Matrix.conjTranspose_circulant, InnerProductSpace.symm_toEuclideanLin_rankOne, MeasureTheory.Lp.coeFn_star, Matrix.diag_conjTranspose, Matrix.conjTranspose_replicateCol, Matrix.dotProduct_self_star_pos_iff, Matrix.IsHermitian.im_star_dotProduct_mulVec_self, MeasureTheory.StronglyMeasurable.star, Matrix.PosDef.dotProduct_mulVec_pos, Matrix.PosDef.re_dotProduct_pos, ZeroAtInftyContinuousMap.coe_star, Matrix.star_mulVec
instSub 📖	CompOp	385 math math: iteratedDerivWithin_sub, MeasureTheory.tendsto_Lp_of_tendsto_ae, StrictConcaveOn.sub, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'', RingHom.ker_evalRingHom, Finset.affineCombination_vsub, mdifferentiableAt_sub_section, MeasureTheory.withDensityᵥ_sub, MeasureTheory.integral_integral_sub', CompactlySupportedContinuousMap.coe_sub, Real.circleAverage_sub, AnalyticWithinAt.sub, Hamming.toHamming_sub, MeasureTheory.Submartingale.sum_mul_sub', MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, TendstoLocallyUniformly.sub, MeasureTheory.Lp.edist_def, MeasureTheory.tendsto_Lp_of_tendstoInMeasure, Set.indicator_sub', ContMDiffWithinAt.sub_section, HasFDerivAtFilter.sub, Matrix.submatrix_sub, MeasureTheory.Supermartingale.sub_martingale, RCLike.wInner_sub_right, cross_cross, MeasureTheory.Lp.dist_def, ContinuousAffineMap.coe_sub, StrictConcaveOn.sub_convexOn, Filter.eventually_sub_nonneg, Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, Function.mulSupport_one_sub', BoxIntegral.integral_sub, IncidenceAlgebra.coe_sub, LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq, Matrix.sub_cons, MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul, HasDerivWithinAt.sub, MeasureTheory.UnifIntegrable.sub, Meromorphic.sub, Antivary.sub_left, MeasureTheory.Submartingale.sum_upcrossingStrat_mul, BoxIntegral.HasIntegral.sub, MeasureTheory.AEFinStronglyMeasurable.sub, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, AnalyticOn.sub, MeasureTheory.eLpNorm_sub_le, HasFDerivAt.sub, UniformFun.toFun_sub, ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero, ValueDistribution.proximity_coe_eq_proximity_sub_const_zero, ZeroHom.coe_sub, MeasureTheory.MemLp.exist_eLpNorm_sub_le, MeasureTheory.StronglyMeasurable.sub, EisensteinSeries.E2_slash_action, DifferentiableOn.sub, Matrix.circulant_sub, Function.Periodic.cuspFunction_sub, LocallyConstant.coe_sub, EisensteinSeries.G2_slash_action, MeasureTheory.AEStronglyMeasurable.sub, ProbabilityTheory.iIndepFun.indepFun_sub_left, ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith, DFinsupp.coe_tsub, ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right₀, deriv_sub, MeasureTheory.AEEqFun.coeFn_sub, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp, cross_cross_eq_smul_sub_smul, MeasureTheory.Lp.edist_toLp_toLp, MeasureTheory.Integrable.tendsto_eLpNorm_condExp, MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd, ContinuousMultilinearMap.norm_image_sub_le, Matrix.empty_sub_empty, LSeries_sub, MeasureTheory.sub_ae_eq_zero, Complex.ofReal_comp_sub, MeasureTheory.Submartingale.sum_mul_sub, MeasureTheory.AEEqFun.mk_sub, measurableSub₂, LSeries.term_sub, Matrix.sub_vecMul, ConvexOn.sub, HasDerivAtFilter.sub, MeasureTheory.VectorMeasure.coe_sub, AffineMap.decomp', ValueDistribution.isBigO_characteristic_sub_characteristic_shift, ContinuousAlternatingMap.coe_sub, Differentiable.sub_iff_right, ContinuousMap.coe_sub, MeasureTheory.StronglyAdapted.sub, ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity, FormalMultilinearSeries.ofScalars_sub, MeasureTheory.lpNorm_sub_comm, groupCohomology.H2π_eq_iff, ContMDiffMap.coe_sub, Hamming.ofHamming_sub, ValueDistribution.logCounting_sub_const, mfderiv_sub, Function.locallyFinsuppWithin.coe_sub, Matrix.vec_sub, MeasureTheory.Integrable.sub, MeasureTheory.Submartingale.sub_supermartingale, ProbabilityTheory.covariance_sub_right, Monovary.sub_right, HasDerivAt.sub, ProbabilityTheory.variance_sub, map_comp_sub, single_sub, Set.piecewise_sub, MeasureTheory.eLpNorm_sub_comm, LeftInvariantDerivation.coe_sub, HasFPowerSeriesWithinOnBall.sub, ProbabilityTheory.iCondIndepFun.indepFun_sub_sub, ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left, UniformConcaveOn.sub, ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left₀, MeasureTheory.lpNorm_sub_le, MulActionHom.coe_sub, AEMeasurable.sub', volume_regionBetween_eq_lintegral', TemperedDistribution.smulLeftCLM_sub, RCLike.wInner_sub_left, CentroidHom.coe_sub, MeasureTheory.UnifTight.sub, MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub', MultilinearMap.map_add_sub_map_add_sub_linearDeriv, ProbabilityTheory.iCondIndepFun.indepFun_sub_left, Filter.Germ.coe_sub, MeasureTheory.Measure.withDensity_sub_of_le, MeasureTheory.lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub, MDifferentiableAt.sub, Poly.coe_sub, SlashInvariantForm.coe_sub, DifferentiableWithinAt.sub, Filter.EventuallyEq.sub_eq, MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le, MeasureTheory.LocallyIntegrable.sub, HasFPowerSeriesWithinAt.sub, lp.coeFn_sub, AlternatingMap.norm_image_sub_le_of_bound, CPolynomialOn.sub, MeasureTheory.Integrable.toL1_sub, mdifferentiableWithinAt_sub_section, ProbabilityTheory.covariance_sub_left, LSeries.term_sub_apply, Differentiable.sub, qExpansion_sub, IsCompactOperator.sub, UniformOnFun.ofFun_sub, Fintype.piFinset_sub, MeasureTheory.eLpNorm_sub_le', AnalyticAt.sub, sub_def, fderiv_sub, ValueDistribution.characteristic_sub_characteristic_inv, CPolynomialAt.sub, BoxIntegral.Integrable.sub, PhragmenLindelof.isBigO_sub_exp_exp, ContMDiffSection.coe_sub, DifferentiableAt.sub_iff_left, MeasureTheory.stoppedValue_sub_eq_sum', Set.MapsTo.sub, intervalIntegral.integral_sub_linear_isLittleO_of_tendsto_ae, ValueDistribution.isBigO_characteristic_sub_characteristic_inv, CuspForm.coe_sub, MeasureTheory.integral_sub', HasStrictDerivAt.sub, MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₂, HahnSeries.SummableFamily.coe_sub, MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le, ProbabilityTheory.HasGaussianLaw.sub, conjneg_sub, sub_comp, ProbabilityTheory.Kernel.integral_integral_sub', HasFPowerSeriesOnBall.sub, translate_sub_right, MeasureTheory.sub_nonneg_ae, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, MeasureTheory.eLpNorm_indicator_sub_indicator, MeromorphicOn.sub, Measurable.sub_stronglyMeasurable, le_analyticOrderAt_sub, ProbabilityTheory.iIndepFun.indepFun_sub_div₀, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, Matrix.cons_sub, ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_div₀, MeromorphicAt.sub, AntivaryOn.sub_right, locallyFinsuppWithin.logCounting_divisor, MultilinearMap.norm_image_sub_le_of_bound, Matrix.blockDiagonal_sub, MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub, variationOnFromTo.sub_self_monotoneOn, Sum.elim_sub_sub, UniformCauchySeqOn.sub, Matrix.cons_sub_cons, sub_bounded_of_bounded_of_bounded, QuadraticMap.coeFn_sub, TestFunction.coe_sub, MeasureTheory.tendsto_eLpNorm_condExp, Function.const_sub, ContDiffMapSupportedIn.coe_sub, sub_dotProduct, CauSeq.coe_sub, DifferentiableOn.sub_iff_right, MeasureTheory.Submartingale.sum_smul_sub', Differentiable.sub_iff_left, Asymptotics.isLittleOTVS_comm, HasMFDerivAt.sub, ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right, HasFDerivWithinAt.sub, Filter.Tendsto.uniformity_sub, LSeriesHasSum.sub, curveIntegralFun_sub, MeasureTheory.SimpleFunc.coe_sub, ProbabilityTheory.iIndepFun.hasGaussianLaw_sub, DifferentiableAt.sub, MeasureTheory.stoppedValue_sub_eq_sum, TendstoUniformlyOn.sub, HasCompactSupport.sub, Asymptotics.IsEquivalent.sub_isLittleO, NormedAddGroupHom.coe_sub, MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess, Set.indicator_compl, MDifferentiable.sub, MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₁, HahnSeries.coeff_sub', DifferentiableAt.sub_iff_right, ValueDistribution.abs_characteristic_sub_characteristic_shift_eqO, HasFPowerSeriesAt.sub, LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn, Function.HasTemperateGrowth.sub, ProbabilityTheory.iIndepFun.indepFun_sub_right, ConvexOn.sub_strictConcaveOn, measurableSub, ContMDiffAt.sub_section, orderedSub, DiffContOnCl.sub, AbsolutelyContinuousOnInterval.sub, Filter.eventuallyEq_iff_sub, Real.isBigO_exp_comp_exp_comp, PhragmenLindelof.isBigO_sub_exp_rpow, volume_regionBetween_eq_integral', LSeriesSummable.sub, Matrix.sub_mulVec, AdicCompletion.val_sub, DFinsupp.coe_sub, ProbabilityTheory.iCondIndepFun.indepFun_sub_right, Antivary.sub_right, MeasureTheory.martingalePart_eq_sum, MeasureTheory.setToFun_sub, birkhoffSum_sub, ContinuousMapZero.coe_sub, UniformOnFun.toFun_sub, fderivWithin_sub, Matrix.vecMul_sub, mDifferentiableOn_sub_section, MeasureTheory.Submartingale.sum_smul_sub, map_comp_sub', ProbabilityTheory.iIndepFun.indepFun_sub_left₀, birkhoffAverage_sub, MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le, Matrix.blockDiag'_sub, IsAddFreimanHom.sub, cuspFunction_sub, TendstoUniformly.sub, OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, Matrix.tail_sub, mdifferentiable_sub_section, LSeries.abscissaOfAbsConv_sub_le, HasFiniteFPowerSeriesAt.sub, Matrix.blockDiag_sub, Matrix.head_sub, MonovaryOn.sub_right, MeasureTheory.LocallyIntegrableOn.sub, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm', MeasureTheory.Martingale.sub, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, MeasureTheory.submartingale_iff_condExp_sub_nonneg, LinearMap.IsAdjointPair.sub, Matrix.blockDiagonal'_sub, update_eq_sub_add_single, ContMDiff.sub_section, Derivation.coe_sub, UniformConvexOn.sub, Matrix.sub_vecMulVec, MeasureTheory.Lp.coeFn_sub, UniformFun.ofFun_sub, EuclideanGeometry.dist_affineCombination, volume_regionBetween_eq_integral, MeasureTheory.FinStronglyMeasurable.sub, Finsupp.coe_tsub, ContinuousLinearMap.coe_sub', WithCStarModule.sub_apply, intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sub, ConcaveOn.sub, SchwartzMap.smulLeftCLM_sub, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, AntivaryOn.sub_left, DFinsupp.mk_sub, LieDerivation.coe_sub, Matrix.of_sub_of, IsLocallyConstant.sub, HasCompactSupport.exist_eLpNorm_sub_le_of_continuous, LieModuleHom.coe_sub, MeasureTheory.eLpNorm_sub_le_of_dist_bdd, ContMDiffOn.sub_section, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, derivWithin_sub, TendstoUniformlyOnFilter.sub, Function.update_sub, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, MeasureTheory.condExp_sub, cross_cross_eq_smul_sub_smul', Finsupp.coe_sub, ModularForm.coe_sub, hammingDist_eq_hammingNorm, Complex.cderiv_sub, curveIntegral_sub, iteratedDeriv_sub, ZeroAtInftyContinuousMap.coe_sub, CurveIntegrable.sub, MeasureTheory.condExpL1_sub, BoundedContinuousFunction.coe_sub, ProbabilityTheory.iIndepFun.indepFun_sub_sub, Asymptotics.IsEquivalent.isLittleO, Memℓp.sub, MeasureTheory.mul_upcrossingsBefore_le, ValueDistribution.log_counting_zero_sub_logCounting_top, AffineMap.coe_sub, HasFiniteFPowerSeriesOnBall.sub, torusMap_sub_center, HasStrictFDerivAt.sub, Matrix.mulVec_sub, Filter.EventuallyEq.sub, MeasureTheory.Adapted.sub, ProbabilityTheory.Kernel.integral_integral_sub'_comp, Function.Periodic.sub, ApproximatesLinearOn.lipschitzOnWith, MeasureTheory.MemLp.sub, StrictConvexOn.sub, Monovary.sub_left, ProbabilityTheory.iIndepFun.indepFun_sub_right₀, intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right, MeasureTheory.Submartingale.sub_martingale, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite, ConcaveOn.sub_strictConvexOn, Measurable.sub', volume_regionBetween_eq_lintegral, DifferentiableOn.sub_iff_left, BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm, ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_sub, MeasureTheory.tendsto_Lp_finite_of_tendsto_ae_of_meas, groupCohomology.H1π_eq_iff, Asymptotics.isBigOTVS_comm, Function.extend_sub, MeasureTheory.Measure.withDensity_sub, MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, MeasureTheory.Submartingale.condExp_sub_nonneg, MeasureTheory.IntegrableAtFilter.sub, Fin.insertNth_sub, AnalyticOnNhd.sub, TendstoLocallyUniformlyOn.sub, ContinuousAlternatingMap.norm_image_sub_le, StrictConvexOn.sub_concaveOn, Fintype.balance_sub, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm, MeasureTheory.MemLp.toLp_sub, Set.indicator_diff, dotProduct_sub, sub_apply, Fin.insertNth_sub_same, MeasureTheory.tendsto_Lp_finite_of_tendsto_ae, Matrix.vecMulVec_sub, TorusIntegrable.sub, Matrix.diag_sub, MonovaryOn.sub_left, MeasureTheory.Supermartingale.sub_submartingale, MeasureTheory.SignedMeasure.rnDeriv_sub
instVAdd 📖	CompOp	33 math math: Set.vadd_set_pi_of_surjective, vaddCommClass, DomAddAct.instVAddCommClassForall_1, Set.vadd_set_univ_pi, Set.vadd_set_pi_of_isAddUnit, Filter.vadd_tendsto_vadd_iff, faithfulVAdd, vaddAssocClass, isCentralVAdd, IsAddUnit.vadd_tendsto_vadd_iff, vadd_def, vadd_comp, DomAddAct.instVAddCommClassForall, faithfulVAdd_at, Function.update_vadd, Function.Periodic.vadd, vaddAssocClass', vadd_univ_pi, Function.vadd_const, instMeasurableConstVAdd, vadd_pi_subset, instIsIsometricVAddForall, Set.piecewise_vadd, instContinuousConstVAddForall, evalAddActionHom_apply, instContinuousVAddForall, Filter.EventuallyEq.const_vadd, measurableVAdd, vaddCommClass', vadd_pi, AddActionHom.coe_vadd, Set.vadd_set_pi, vadd_apply
instZero 📖	CompOp	787 math math: LinearGrowth.linearGrowthSup_zero, Matrix.replicateCol_zero, LieHom.coe_zero, AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq, HolderWith.zero, Function.const_nonpos_of_nonpos, MeasureTheory.llr_self, fderivWithin_ofNat, logDeriv_const, exists_contMDiffMap_zero_one_of_isClosed, Polynomial.ofFn_zero, Function.mulSupport_zero, MeasureTheory.Measure.rnDeriv_zero, NumberField.mixedEmbedding.logMap_one, Asymptotics.isBigO_zero_right_iff, EisensteinSeries.gammaSet_div_gcd_to_gammaSet10_bijection, MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant, SchwartzMap.coe_zero, HahnSeries.coeff_fun_eq_zero_iff, fderiv_intCast, AlternatingMap.constLinearEquivOfIsEmpty_symm_apply, cfcₙ_zero, Matrix.Nondegenerate.eq_zero_of_ortho, fderivWithin_one, FormalMultilinearSeries.ofScalars_series_eq_zero_of_scalar_zero, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, VectorField.lieBracketWithin_zero_left, Finset.piAntidiag_zero, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, MeasureTheory.lintegral_eq_zero_iff, instZeroLEOneClass, Hamming.ofHamming_zero, Matrix.zero_mulVec, MeasureTheory.eLpNorm'_zero', SchwartzMap.coeFn_zero, derivWithin_const, Matrix.empty_vecMul, MeasureTheory.Lp.eq_zero_iff_ae_eq_zero, PiTensorProduct.subsingletonEquiv_symm_apply, ConvexOn.uniformConvexOn_zero, Matrix.hadamard_one_eq_zero_iff, NumberField.mixedEmbedding.norm_eq_zero_iff', ProbabilityTheory.condVar_const, MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real, Set.image_single_uIcc_right, Topology.CWComplex.continuousOn, LSeries_eventually_eq_zero_iff', fwdDiff_iter_pow_eq_zero_of_lt, zero_memℓp, Fintype.balance_zero, derivWithin_natCast, Multiset.Nat.antidiagonalTuple_zero_right, PadicInt.nthHom_zero, Matrix.conjTranspose_mul_self_mulVec_eq_zero, Matrix.replicateRow_zero, BoxIntegral.BoxAdditiveMap.zero_apply, Filter.eventually_sub_nonneg, Bornology.isVonNBounded_pi_iff, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, ProbabilityTheory.Kernel.ae_null_of_compProd_null, ProbabilityTheory.mgf_zero_fun, lp.eq_zero_iff_coeFn_eq_zero, NonUnitalStarRingHom.coe_zero, LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq, hasDerivWithinAt_zero, MeasureTheory.FiniteMeasure.zero_testAgainstNN, LieModule.Weight.coe_zero, cross_self, CurveIntegrable.zero, iteratedDerivWithin_const_zero, LieAlgebra.coe_zeroRootSubalgebra, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, LieModule.isNilpotent_toEnd_genWeightSpace_zero, Topology.RelCWComplex.pairwiseDisjoint', dotProduct_star_self_eq_zero, single_nonpos, Finsupp.linearCombination_zero_apply, UpperHalfPlane.prod_eq_zero_iff, Sum.elim_zero_zero, IntervalIntegrable.zero, ContinuousLinearMap.coe_zero', MeasureTheory.pdf_of_not_haveLebesgueDecomposition, Asymptotics.isBigOWith_zero_right_iff, UniformConvergenceCLM.coe_zero, ProbabilityTheory.Kernel.compProd_null, ModularForm.norm_eq_zero_iff, groupCohomology.cocycles₂.d₂₃_apply, MeasureTheory.MemLp.zero, MeasureTheory.eLpNormEssSup_zero, fderivWithin_intCast, PartitionOfUnity.nonneg', MeasureTheory.tilted_zero, ZMod.completedLFunction_zero, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, PiLp.isBoundedSMulSeminormedAddCommGroupToPi, HahnSeries.ofSuppBddBelow_zero, fderiv_ofNat, LieModule.chainTop_zero, MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite, MeasureTheory.withDensity_eq_zero_iff, fderivWithin_zero, MeasureTheory.upcrossingsBefore_zero', MeasureTheory.withDensity_zero, Set.range_zero, iteratedFDerivWithin_succ_const, MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero', MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero, ContinuousMultilinearMap.curry0_apply, ProbabilityTheory.Kernel.coe_zero, hasFDerivAtFilter_zero, LocallyConstant.coe_zero, VectorField.lieBracketWithin_zero_right, IsLocalExtr.lineDeriv_eq_zero, Matrix.isNilpotent_iff_forall_row, Topology.RelCWComplex.source_eq, LieModule.iSup_ucs_le_genWeightSpace_zero, Matrix.diag_zero, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite, MeasureTheory.lintegral_zero_fun, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, Topology.RelCWComplex.continuousOn, exists_continuous_zero_one_of_isClosed, RootPairing.Base.pos_or_neg_of_sum_smul_root_mem, stdSimplex_subset_closedBall, ValueDistribution.logCounting_const_zero, CStarMatrix.norm_def', Sum.elim_single_zero, Topology.RelCWComplex.union', hasCompactSupport_iff_eventuallyEq, torusMap_zero_radius, ValueDistribution.proximity_nonneg, MeasureTheory.VectorMeasure.coe_zero, HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group, Representation.IntertwiningMap.coe_zero, hasDerivAtFilter_zero, IncidenceAlgebra.coe_zero, uncurry_single_single, Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero, MvPowerSeries.HasEval.zero, Finset.piAntidiag_empty, dotProduct_eq_zero, ProbabilityTheory.cgf_zero_fun, single_zero, VectorField.mlieBracket_zero_right, Set.indicator_empty', WithCStarModule.zero_apply, gauge_zero', ModularFormClass.levelOne_neg_weight_eq_zero, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, MeasureTheory.condExp_zero, conjneg_pos, ProbabilityTheory.Kernel.rnDeriv_singularPart, linearIndependent_zero_iff, Matrix.separatingLeft_def, DistribMulActionHom.coe_zero, VectorField.lieBracketWithin_self, Matrix.gram_zero, torusMap_eq_center_iff, curveIntegralFun_refl, TrivSqZeroExt.fst_comp_inr, MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg, MeasureTheory.sub_ae_eq_zero, MeasureTheory.eLpNorm_eq_zero_iff, ProbabilityTheory.covariance_zero_right, EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq, PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay, PhragmenLindelof.eq_zero_on_vertical_strip, PhragmenLindelof.eq_zero_on_quadrant_IV, Finset.Nat.antidiagonalTuple_zero_right, OrderAddMonoidHom.coe_zero, UpperHalfPlane.zero_form_isBoundedAtImInfty, ZeroAtInftyContinuousMap.coe_zero, Asymptotics.IsLittleOTVS.zero, NonarchAddGroupSeminorm.coe_zero, NumberField.canonicalEmbedding.integerLattice.inter_ball_finite, LieModule.Weight.IsZero.eq, Set.image_single_Icc_left, Real.logb_zero_left_eq_zero, lp.coeFn_zero, SimpleGraph.lapMatrix_mulVec_const_eq_zero, MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero, ProbabilityTheory.moment_zero, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, ValueDistribution.logCounting_const, MvPolynomial.eval₂Hom_zero_apply, deriv_zero, UniformFun.toFun_zero, derivWithin_ofNat, Asymptotics.isEquivalent_zero_iff_eventually_zero, Function.locallyFinsuppWithin.eq_zero_codiscreteWithin, zero_dotProduct, iteratedFDeriv_succ_const, MulActionHom.coe_zero, Matrix.ker_mulVecLin_eq_bot_iff, extDeriv_extDeriv, ContinuousMultilinearMap.range_toUniformOnFun, MeasureTheory.stronglyAdapted_zero, cross_anticomm', MeasureTheory.eLpNorm_zero, EisensteinSeries.gammaSet_one_mem_iff, LinearGrowth.linearGrowthInf_zero, ContMDiffSection.coe_zero, fderiv_one, MeasureTheory.measureReal_zero, MeasureTheory.lintegral_eq_zero_iff', Function.Exact.comp_eq_zero, LieModule.chainBot_zero, MeasureTheory.martingale_zero, Polynomial.fwdDiff_iter_degree_add_one_eq_zero, MeasureTheory.SimpleFunc.coe_zero, TorusIntegrable.torusIntegrable_zero_radius, MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero, hasSum_zero_iff_of_nonneg, Function.comp_eq_zero_iff, extDerivWithin_extDerivWithin_eqOn, SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero, UnitAddTorus.mFourier_zero, memHolder_zero, exists_bounded_zero_one_of_closed, Asymptotics.IsLittleOTVS.pi, SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero, Sum.nonneg_elim_iff, Function.const_nonneg_of_nonneg, ContDiffMapSupportedIn.zero_on_compl', Height.logHeight_zero, ContinuousMultilinearMap.hasBasis_nhds_zero, translate_zero_right, zero_apply, compContinuousLinearMap_zero, exists_continuous_one_zero_of_isCompact, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, LinearMap.toMvPolynomial_zero, MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero', indicator_meas_zero, MeasureTheory.mlconvolution_zero, Module.rankAtStalk_eq_zero_iff_subsingleton, Filter.zero_zeroAtFilter, hammingDist_zero_right, ProbabilityTheory.centralMoment_zero, MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg, LSeriesSummable_zero, instIsBoundedSMul', Matrix.blockDiag'_zero, Finsupp.single_eq_update, DFinsupp.mk_zero, ContDiffMapSupportedIn.zero_on_compl, nnHolderNorm_zero, gauge_closure_zero, exists_continuous_nonneg_pos, ContinuousAlternatingMap.map_zero, Set.indicator_zero_preimage, ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall, Function.support_fun_curry, MeasureTheory.FiniteMeasure.coeFn_zero, Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg, MeasureTheory.finStronglyMeasurable_zero, Function.locallyFinsuppWithin.restrict_eqOn_compl, Matrix.fromCols_replicateCol0_isTotallyUnimodular_iff, contMDiffOn_zero, contMDiffWithinAt_zero, Matrix.of_zero, ContinuousAlternatingMap.constOfIsEmptyLIE_symm_apply, gauge_empty, PolynomialLaw.toFun_zero, ProbabilityTheory.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero, NumberField.house.exists_ne_zero_int_vec_house_le, Matrix.blockDiag_zero, Int.fract_int, MeasureTheory.condExp_of_not_integrable, VectorField.mpullback_zero, MeasureTheory.condExp_of_not_le, PhragmenLindelof.eq_zero_on_horizontal_strip, HahnSeries.ofSuppBddBelow_eq_zero, ContinuousMap.coe_zero, RCLike.wInner_zero_right, eisSummand_of_gammaSet_eq_divIntMap, LieModule.Weight.coe_eq_zero_iff, PolynomialLaw.zero_def, List.Nat.antidiagonalTuple_zero_right, MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant, Matrix.toMvPolynomial_zero, VectorField.mlieBracketWithin_zero_right, Function.support_extend_zero_subset, Finset.weightedVSubVSubWeights_self, ProbabilityTheory.mgf_zero_measure, Topology.CWComplex.union', ContDiffMapSupportedIn.structureMapLM_apply_withOrder, MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero, Matrix.PosSemidef.toLinearMap₂'_zero_iff, Ordinal.nfp_zero, MultilinearMap.map_zero, Polynomial.fwdDiff_iter_eq_zero_of_degree_lt, Height.mulHeight_zero, ExteriorAlgebra.liftAlternating_one, Asymptotics.superpolynomialDecay_zero, Asymptotics.isBigO_const_iff, MeasureTheory.Measure.measure_ae_null_of_prod_null, MeasureTheory.BorelCantelli.process_zero, AnalyticOnNhd.eqOn_zero_of_preconnected_of_mem_closure, birkhoffSum_zero', gauge_of_subset_zero, UniformFun.ofFun_zero, Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero, ProbabilityTheory.HasCondSubgaussianMGF.zero, MeasureTheory.eLpNorm'_zero, VectorField.mpullbackWithin_zero, exists_continuous_zero_one_of_isCompact', Function.support_eq_empty_iff, Probability.cauchyPDF_scale_zero, toMeromorphicNFOn_of_not_meromorphicOn, iteratedDeriv_const_zero, Function.const_nonpos, ProbabilityTheory.variance_zero, AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, instIsReducedForall, hasFDerivWithinAt_zero, ValueDistribution.characteristic_eventually_nonneg, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, JacobsonNoether.exist_pow_eq_zero_of_le, tsum_extend_zero, Set.image_single_Ioo_left, MeasureTheory.Measure.bind_zero_right, Set.indicator_zero', differentiableAt_zero, zero_def, associator_eq_zero_iff_associative, Topology.CWComplex.source_eq, Topology.CWComplex.pairwiseDisjoint', conjneg_zero, Filter.EventuallyEq.sub_eq, VectorField.lieBracket_zero_right, dotProduct_self_eq_zero, MeasureTheory.condLExp_of_not_le, HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero, Set.image_single_Ioo_right, Probability.cauchyPDFReal_scale_zero, Set.indicator_eq_zero', ExpGrowth.expGrowthSup_zero, MeasureTheory.condExp_def, ConcaveOn.uniformConcaveOn_zero, Polynomial.toFn_zero, ProbabilityTheory.condVar_zero, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, hasStrictFDerivAt_zero, continuousMultilinearCurryFin0_apply, Function.zero_of_even_and_odd, LieAlgebra.rootSpace_zero_eq, VectorField.mlieBracketWithin_self, Sigma.curry_single, ProbabilityTheory.condVar_of_not_le, conjneg_nonpos, RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, fderivWithin_const, CauSeq.coe_zero, Matrix.mulVec_zero, hasSum_extend_zero, Behrend.sphere_zero_subset, GroupSeminorm.coe_zero, BumpCovering.nonneg', fderiv_natCast, ProbabilityTheory.gaussianPDF_zero_var, Topology.CWComplex.mapsTo', fderiv_const, comp_zero, Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, ContMDiffMap.coe_zero, mem_parallelepiped_iff, MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter, NonUnitalStarAlgHom.coe_zero, Matrix.tail_zero, MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top, instSMulPosReflectLT, notMem_tsupport_iff_eventuallyEq, differentiable_zero, ContMDiff.extend_zero, MvPolynomial.eval_zero, ModularForm.coe_eq_zero_iff, VectorField.mlieBracket_zero_left, Matrix.replicateRow_eq_zero, ProbabilityTheory.evariance_zero, Set.indicator_ae_eq_zero, MeasureTheory.withDensity_eq_zero, Matrix.vecMul_conjTranspose_mul_self_eq_zero, instSMulPosStrictMono, ContinuousAffineMap.coe_zero, Real.logb_one_left_eq_zero, Matrix.circulant_zero, zero_cpow_eq_nhds, zero_anti, hammingNorm_eq_zero, continuous_zero, ContinuousAlternatingMap.hasBasis_nhds_zero, MvPolynomial.eval₂_zero_apply, Matrix.exists_mulVec_eq_zero_iff, TestFunction.coe_zero, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Seminorm.coe_bot, curveIntegralFun_fun_zero, IsOpen.measure_eq_biSup_integral_continuous, HasCompactSupport.eq_zero_or_finiteDimensional, MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular, Homotopy.ofEq_hom, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, Matrix.vec_eq_zero_iff, Sigma.curry_zero, Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero, Matrix.ker_toLin'_eq_bot_iff, derivWithin_intCast, VectorField.lieBracket_self, Matrix.zero_vecMul, LieModule.chainBotCoeff_zero, Topology.RelCWComplex.map_zero_mem_openCell, MeasureTheory.sub_nonneg_ae, MvPolynomial.eval₂Hom_zero, MvPolynomial.aeval_zero, MeasureTheory.stronglyAdapted_zero', MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition, Ordinal.deriv_zero, Asymptotics.isBigOTVS_pi, zero_comp, MvPowerSeries.rescale_zero, instIsBoundedSMul, List.aestronglyMeasurable_sum, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, MeasureTheory.OuterMeasure.boundedBy_zero, Matrix.blockDiagonal'_zero, uniformConcaveOn_zero, ContinuousAddMonoidHom.coe_zero, fderivWithin_fun_const, Matrix.vec_zero, MeasureTheory.Measure.rnDeriv_def, MeasureTheory.Lp.coeFn_nonneg, conjneg_eq_zero, Set.image_single_Icc_right, derivWithin_one, Matrix.zero_le_one_row, Matrix.cons_zero_zero, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, HasCompactSupport.tsupport_extend_zero_subset, SlashInvariantForm.coe_zero, MeasureTheory.Lp.simpleFunc.coeFn_zero, eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup, Tactic.ComputeAsymptotics.Majorized.zero, LieModule.isCompl_genWeightSpace_zero_posFittingComp, MeasureTheory.condExpIndSMul_nonneg, ProbabilityTheory.Kernel.ae_null_of_comp_null, MeasureTheory.OuterMeasure.coe_zero, Matrix.cons_eq_zero_iff, Matrix.one_hadamard_eq_zero_iff, Function.extend_zero, MeasureTheory.Measure.rnDeriv_singularPart, ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl, UpperHalfPlane.eq_zero_of_frequently, ProbabilityTheory.Kernel.HasSubgaussianMGF.zero, exists_continuous_zero_one_of_isCompact, supportDiscreteWithin_iff_locallyFiniteWithin, HasCompactSupport.continuous_extend_zero, MeasureTheory.convolution_zero, ENNReal.limsup_eq_zero_iff, MeasureTheory.pdf_of_not_aemeasurable, CompactlySupportedContinuousMap.coe_zero, Matrix.blockDiagonal_zero, Function.support_curry, List.aemeasurable_sum, IsLocalMax.lineDeriv_eq_zero, indicator_ae_eq_restrict_compl, IsLocallyConstant.zero, curveIntegral_zero, gradient_const', Asymptotics.isLittleO_zero_right_iff, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, MeasureTheory.lpNorm_zero, HahnSeries.coeff_zero', Set.preimage_zero, Matrix.vecMulVec_zero, Function.support_disjoint_iff, Function.noZeroSMulDivisors, Function.update_zero, CentroidHom.coe_zero, Finsupp.coe_eq_zero, Projectivization.cross_mk, deriv_one, MeasureTheory.SimpleFunc.setToSimpleFunc_zero, MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl, MeasureTheory.condExp_of_not_sigmaFinite, ProbabilityTheory.gaussianPDFReal_zero_var, ContinuousAlternatingMap.coe_zero, Matrix.exists_vecMul_eq_zero_iff, measurable_zero, LinearEquiv.coe_zero, EisensteinSeries.D2_one, Finset.piAntidiag_empty_zero, MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim, Ordinal.deriv_zero_left, ZeroHom.single_apply, LieModule.genWeightSpace_zero_normalizer_eq_self, fderivWithin_natCast, MeasureTheory.zero_lconvolution, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis, Set.image_single_Ico_left, Matrix.self_mul_conjTranspose_mulVec_eq_zero, AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype, MeasureTheory.L1.SimpleFunc.setToL1S_zero_left, ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis, Matrix.fromRows_replicateRow0_isTotallyUnimodular_iff, RootPairing.Base.exists_root_eq_sum_int, Set.indicator_preimage, Function.const_pos, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, Filter.Germ.coe_zero, hammingNorm_zero, MeasureTheory.AEEqFun.coeFn_zero, deriv_natCast, ProbabilityTheory.condVar_of_sigmaFinite, torusIntegral_radius_zero, Sigma.uncurry_single_single, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, Ordinal.nfp_zero_left, linearIndepOn_zero_iff, PhragmenLindelof.eq_zero_on_quadrant_II, CuspForm.coe_zero, InnerProductSpace.gramSchmidt_zero, Set.eqOn_indicator', cfc_zero, Topology.RelCWComplex.mapsTo, Sum.elim_zero_single, Set.image_single_uIcc_left, List.periodic_sum, exists_smooth_zero_one_of_isClosed, iteratedFDeriv_zero_fun, RCLike.wInner_zero_left, List.measurable_sum, Filter.eventuallyEq_iff_sub, MeasureTheory.withDensityᵥ_zero, HahnSeries.SummableFamily.coe_zero, fderiv_zero, MeasureTheory.setToFun_zero, AlternatingMap.map_zero, NumberField.mixedEmbedding.unit_smul_eq_zero, HahnSeries.mk_eq_zero, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg, Matrix.PosSemidef.dotProduct_mulVec_zero_iff, eHolderNorm_zero, single_nonneg, derivWithin_fun_const, Matrix.updateCol_zero_zero, hasDerivAt_zero, Matrix.of_symm_single, instSMulPosMono, LSeries_zero, Topology.RelCWComplex.disjointBase', Matrix.single_eq_of_single_single, Function.ExtendByZero.hom_apply, contMDiff_zero, MeasureTheory.tilted_zero', NumberField.mixedEmbedding.logMap_real, deriv_intCast, eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group, UpperHalfPlane.mul_eq_zero_iff, MeasureTheory.condExp_of_sigmaFinite, HasCompactSupport.extend_zero, Function.support_extend_zero, Matrix.vecMulVec_eq_zero, LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian, LieModuleHom.coe_zero, MeasureTheory.eLpNorm'_eq_zero_iff, Hamming.toHamming_zero, LieModule.zero_genWeightSpace_eq_top_of_nilpotent', Function.support_zero, Matrix.Nondegenerate.eq_zero_of_ortho', LieModule.iSup_ucs_eq_genWeightSpace_zero, Function.const_zero, AEMeasurable.exists_measurable_nonneg, curry_single, Function.const_nonneg, Matrix.isNilpotent_iff, MeasureTheory.integral_zero', FormalMultilinearSeries.comp_rightInv, exists_continuous_one_zero_of_isCompact_of_isGδ, differentiableOn_zero, Projectivization.cross_mk_of_ne, Asymptotics.isTheta_zero_left, LieModule.chainTopCoeff_zero, derivWithin_zero, Matrix.nondegenerate_def, list_sum_apply, Matrix.replicateCol_eq_zero, ContinuousMultilinearMap.toUniformOnFun_toFun, IsCompact.measure_eq_biInf_integral_hasCompactSupport, ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, WittVector.bind₁_zero_wittPolynomial, MeasureTheory.Lp.coeFn_zero, LeftInvariantDerivation.coe_zero, FormalMultilinearSeries.ofScalars_series_eq_zero, hammingNorm_lt_one, ExteriorAlgebra.liftAlternating_algebraMap, MultilinearMap.dfinsuppFamily_zero, map_comp_zero, LSeries_eq_zero_of_abscissaOfAbsConv_eq_top, birkhoffAverage_zero', AffineMap.coe_zero, Seminorm.coe_zero, Asymptotics.isTheta_zero_right, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable, Matrix.mulVec_empty, AddGroupSeminorm.coe_zero, Associates.count_reducible, MeasureTheory.submartingale_iff_condExp_sub_nonneg, ProbabilityTheory.condVar_of_not_sigmaFinite, MeasureTheory.stronglyMeasurable_zero, Matrix.diag_list_sum, Matrix.zero_vecMulVec, Set.image_single_Ioc_left, single_eq_zero_iff, hasFDerivAt_zero, MeasureTheory.Measure.measure_prod_null, conjneg_nonneg, MeasureTheory.Measure.measure_support_eq_zero_iff, Fin.insertNth_zero_right, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', dotProduct_eq_zero_iff, LieDerivation.coe_zero, LieAlgebra.toLieSubmodule_le_rootSpace_zero, isCompactOperator_zero, MeasureTheory.condLExp_def, MeasureTheory.aefinStronglyMeasurable_zero, hasStrictDerivAt_zero, ProbabilityTheory.Kernel.withDensity_zero, dotProduct_self_star_eq_zero, iteratedFDerivWithin_const_of_ne, Function.ExtendByZero.linearMap_apply, toMeromorphicNFAt_of_not_meromorphicAt, ValueDistribution.logCounting_eventually_nonneg, ZeroHom.coe_single, HasCompactSupport.tsupport_extend_zero, jacobi_cross, MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero, Matrix.IsHermitian.eigenvalues_eq_zero_iff, NonUnitalAlgHom.coe_zero, Matrix.single_mulVec, MeasureTheory.condExpL1_zero, iteratedFDerivWithin_zero_fun, MeasureTheory.Measure.MutuallySingular.rnDeriv_ae_eq_zero, MeasureTheory.Measure.LebesgueDecomposition.zero_mem_measurableLE, Asymptotics.isEquivalent_zero_iff_isBigO_zero, PseudoMetric.coe_bot, MeasureTheory.eLpNormEssSup_eq_zero_iff, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero', NonUnitalRingHom.coe_zero, MultilinearMap.constLinearEquivOfIsEmpty_symm_apply, HasCompactSupport.zero, ProbabilityTheory.condVar_of_not_integrable, AdicCompletion.val_zero, Derivation.coe_zero, Matrix.vecMul_self_mul_conjTranspose_eq_zero, BoundedContinuousFunction.coe_zero, hammingDist_zero_left, instSMulPosReflectLE, ProbabilityTheory.HasSubgaussianMGF.zero, IsLocalMin.lineDeriv_eq_zero, Set.piecewise_eq_indicator, NumberField.mixedEmbedding.fundamentalCone.zero_mem_compactSet, Module.rankAtStalk_eq_zero_of_subsingleton, Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero, PhragmenLindelof.eq_zero_on_quadrant_I, List.stronglyMeasurable_sum, Matrix.separatingRight_def, RestrictedProduct.nhds_zero_eq_map_structureMap, ContinuousMultilinearMap.map_zero, QuadraticMap.coeFn_zero, MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero, Set.image_single_Ico_right, ExpGrowth.expGrowthInf_zero, Function.const_eq_zero, MeasureTheory.predictablePart_zero, qExpansion_zero, Set.image_single_Ioc_right, dotProduct_zero, Topology.CWComplex.mapsTo, TorusIntegrable.function_integrable, MeasureTheory.lconvolution_zero, Matrix.submatrix_zero, fderiv_fun_const, ENNReal.ae_eq_zero_of_lintegral_rpow_eq_zero, VectorField.mlieBracketWithin_zero_left, ProbabilityTheory.covariance_zero_left, Function.locallyFinsuppWithin.coe_zero, Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, MvPowerSeries.rescale_zero_apply, ModularForm.coe_zero, RootPairing.GeckConstruction.h_eq_diagonal, MeasureTheory.DominatedFinMeasAdditive.zero, torusMap_sub_center, Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, NumberField.mixedEmbedding.logMap_zero, MeasureTheory.lpNorm_eq_zero, HahnSeries.zero_ofSuppBddBelow, NormedAddGroupHom.coe_zero, SeminormedAddGroup.tendstoUniformlyOn_zero, ProbabilityTheory.cgf_zero_measure, MeasureTheory.condLExp_of_not_sigmaFinite, fwdDiff_iter_sum_mul_pow_eq_zero, VectorField.lieBracket_zero_left, tsupport_zero, Matrix.zero_empty, Sigma.uncurry_zero, HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup, MeasureTheory.zero_convolution, MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero, MeasureTheory.Measure.rnDeriv_eq_zero, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, Pretrivialization.coe_symm_of_notMem, zero_mono, EisensteinSeries.gammaSetDivGcdEquiv_eq, VectorField.mlieBracket_self, summable_extend_zero, ContinuousMultilinearMap.isUniformInducing_toUniformOnFun, seminormFromConst_seq_zero, Function.const_neg', MeasureTheory.weightedSMul_zero_measure, MeasureTheory.aestronglyMeasurable_zero, LinearMap.isAdjointPair_zero, Matrix.diagonal_zero', MeasureTheory.Lp.simpleFunc.coeFn_nonneg, MeromorphicAt.frequently_zero_iff_eventuallyEq_zero, LSeries_eq_zero_iff, PhragmenLindelof.eq_zero_on_quadrant_III, Matrix.updateRow_zero_zero, Matrix.vecMul_zero, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, Matrix.diag_single_of_ne, associator_eq_zero, NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union, ENNReal.essSup_eq_zero_iff, Finsupp.linearCombination_zero, conjneg_neg', MeasureTheory.FinMeasAdditive.zero, EisensteinSeries.D2_T, tsupport_eq_empty_iff, ProbabilityTheory.truncation_zero, Asymptotics.isLittleOTVS_pi, Finsupp.coe_zero, MeasureTheory.Measure.coe_zero, TrivSqZeroExt.snd_comp_inl, UniformOnFun.zero_apply, Matrix.head_zero, MeasureTheory.Submartingale.condExp_sub_nonneg, UniformOnFun.toFun_zero, Finset.sum_eq_sum_extend, AnalyticOnNhd.eqOn_zero_or_eventually_ne_zero_of_preconnected, MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite, MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc, Asymptotics.IsBigOTVS.pi, differentiableWithinAt_zero, Sum.elim_nonpos_iff, EisensteinSeries.mem_gammaSet_one, Int.Matrix.exists_ne_zero_int_vec_norm_le, seminormFromConst_seq_nonneg, ProbabilityTheory.Kernel.comp_null, Matrix.isNilpotent_iff_forall_col, deriv_ofNat, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj, MeasureTheory.condExpL2_indicator_nonneg, groupCohomology.cocycles₁.d₁₂_apply, Topology.RelCWComplex.map_zero_mem_closedCell, Function.disjoint_support_iff, uniformConvexOn_zero, MeasureTheory.zero_mlconvolution, parallelepiped_single, ContDiffMapSupportedInClass.map_zero_on_compl, noZeroSMulDivisors, MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero, contMDiffAt_zero, ContDiffMapSupportedIn.coe_zero, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable, Int.Matrix.exists_ne_zero_int_vec_norm_le', curveIntegralFun_zero, HahnSeries.BddBelow_zero, ContinuousMapZero.coe_zero, iteratedFDeriv_const_of_ne, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff, DFinsupp.coe_zero, continuousMultilinearCurryFin1_apply, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero, MultilinearMap.piFamily_zero, MeasureTheory.Measure.sum_extend_zero
prod 📖	CompOp	18 math math: AddMonoidHom.coe_prod, AddHom.coe_prod, StarAlgHom.coe_prod, MulHom.coe_prod, NonUnitalAlgHom.prod_apply, TendstoLocallyUniformlyOn.piProd, AlgHom.coe_prod, prod_snd_fst, NonUnitalAlgHom.coe_prod, LinearMap.coe_prod, NonUnitalAlgHom.prod_toFun, TendstoLocallyUniformly.piProd, NonUnitalStarAlgHom.coe_prod, prod_fst_snd, LinearMap.prod_apply, ContinuousAffineMap.coe_prod, AffineMap.coe_prod, MonoidHom.coe_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	instAdd	—	—
add_comp 📖	mathematical	—	instAdd	—	—
add_def 📖	mathematical	—	instAdd	—	—
comp_one 📖	mathematical	—	instOne	—	—
comp_zero 📖	mathematical	—	instZero	—	—
div_apply 📖	mathematical	—	instDiv	—	—
div_comp 📖	mathematical	—	instDiv	—	—
div_def 📖	mathematical	—	instDiv	—	—
inv_apply 📖	mathematical	—	instInv	—	—
inv_comp 📖	mathematical	—	instInv	—	—
inv_def 📖	mathematical	—	instInv	—	—
mul_apply 📖	mathematical	—	instMul	—	—
mul_comp 📖	mathematical	—	instMul	—	—
mul_def 📖	mathematical	—	instMul	—	—
neg_apply 📖	mathematical	—	instNeg	—	—
neg_comp 📖	mathematical	—	instNeg	—	—
neg_def 📖	mathematical	—	instNeg	—	—
one_apply 📖	mathematical	—	instOne	—	—
one_comp 📖	mathematical	—	instOne	—	—
one_def 📖	mathematical	—	instOne	—	—
pow_apply 📖	mathematical	—	instPow	—	—
pow_comp 📖	mathematical	—	instPow	—	—
pow_def 📖	mathematical	—	instPow	—	—
prod_fst_snd 📖	mathematical	—	prod	—	—
prod_snd_fst 📖	mathematical	—	prod	—	—
smul_apply 📖	mathematical	—	instSMul	—	—
smul_comp 📖	mathematical	—	instSMul	—	—
smul_def 📖	mathematical	—	instSMul	—	—
star_apply 📖	mathematical	—	Star.star instStarForall	—	—
star_def 📖	mathematical	—	Star.star instStarForall	—	—
sub_apply 📖	mathematical	—	instSub	—	—
sub_comp 📖	mathematical	—	instSub	—	—
sub_def 📖	mathematical	—	instSub	—	—
vadd_apply 📖	mathematical	—	HVAdd.hVAdd instHVAdd instVAdd	—	—
vadd_comp 📖	mathematical	—	HVAdd.hVAdd instHVAdd instVAdd	—	—
vadd_def 📖	mathematical	—	HVAdd.hVAdd instHVAdd instVAdd	—	—
zero_apply 📖	mathematical	—	instZero	—	—
zero_comp 📖	mathematical	—	instZero	—	—
zero_def 📖	mathematical	—	instZero	—	—

---

← Back to Index