Pi

📁 Source: Mathlib/Algebra/Group/Action/Pi.lean

Statistics

Metric	Count
Definitions hasSMul, hasVAdd, addAction, addAction', mulAction, mulAction', smul', vadd'	8
Theorems extend_smul, extend_vadd, smulCommClass, update_smul, update_vadd, vaddCommClass, faithfulSMul, faithfulSMul_at, faithfulVAdd, faithfulVAdd_at, isCentralScalar, isCentralVAdd, isScalarTower, isScalarTower', isScalarTower'', smulCommClass, smulCommClass', smulCommClass'', smul_apply', smul_def', vaddAssocClass, vaddAssocClass', vaddAssocClass'', vaddCommClass, vaddCommClass', vaddCommClass'', vadd_apply', vadd_def', piecewise_smul, piecewise_vadd	30
Total	38

Function

Definitions

Name	Category	Theorems
hasSMul 📖	CompOp	443 math math: AnalyticWithinAt.const_smul, ArithmeticFunction.vonMangoldt.residueClass_eq, AffineIndependent.smul, MeasureTheory.AEEqFun.coeFn_smul, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', MeasureTheory.eLpNormEssSup_const_smul_le, MeasureTheory.ennreal_smul_extend, LieDerivation.coe_smul, ModularForm.smul_slash, MeasureTheory.condExpL1_smul, Matrix.circulant_smul, MeasureTheory.Martingale.smul, Matrix.smul_vecMulVec, IncidenceAlgebra.coe_constSMul, MeasureTheory.eLpNormEssSup_const_smul, AffineMap.coe_smul, curveIntegral_smul, tendsto_tsum_div_pow_atTop_integral, Matrix.det_smul_inv_mulVec_eq_cramer, MeasureTheory.Measure.rnDeriv_smul_right', Matrix.single_vecMul, MeasureTheory.VectorMeasure.coe_smul, ModularForm.mul_slash, MeasureTheory.FinStronglyMeasurable.const_smul, MeasureTheory.AEStronglyMeasurable.const_smul, Rep.diagonalSuccIsoFree_inv_hom_single, AEMeasurable.const_smul, Embedding.coe_smul, Matrix.diag_smul, DilationEquiv.smulTorsor_symm_apply, HasFPowerSeriesWithinAt.const_smul, LocallyConstant.coe_smul, ZeroAtInftyContinuousMap.coe_smul, WeierstrassCurve.Projective.addY_smul, MeasureTheory.HasFiniteIntegral.smul_enorm, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, AffineBasis.coe_smul, stdSimplex_fin_two, deriv_const_smul, WeierstrassCurve.Projective.dblU_smul, curveIntegralFun_smul, ContinuousLinearMap.coe_smul', LSeriesSummable.smul, Matrix.submatrix_smul, Matrix.vecMul_vecMulVec, curveIntegrable_smul_iff, WeierstrassCurve.Projective.Point.toAffine_smul, ModularForm.prod_slash, hasFDerivWithinAt_comp_smul_iff_smul, MeasureTheory.condLExp_smul, MeasureTheory.smul_convolution, MeasureTheory.Measure.rnDeriv_smul_right, MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top', Conformal.const_smul, Module.Basis.toMatrix_smul, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, fderiv_const_smul_field, WeierstrassCurve.Projective.addX_smul, InnerProductSpace.HarmonicAt.const_smul, CircleIntegrable.const_smul, WeierstrassCurve.Projective.smul_equiv_smul, ModularForm.prod_slash_sum_weights, WeierstrassCurve.Projective.add_of_Z_eq_zero, WeierstrassCurve.Projective.dblXYZ_smul, Matrix.det_updateRow_add_smul_self, differentiableAt_smul_iff, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, HasFPowerSeriesOnBall.const_smul, HasStrictFDerivAt.const_smul, ProbabilityTheory.HasGaussianLaw.smul, extDeriv_fun_smul, SlashInvariantForm.coe_smulℝ, EisensteinSeries.E2_slash_action, BoxIntegral.unitPartition.integralSum_eq_tsum_div, MeasureTheory.convolution_smul, Matrix.updateRow_eq_transvection, segment_single_subset_stdSimplex, tendsto_card_div_pow_atTop_volume, WeierstrassCurve.Projective.addXYZ_smul, Asymptotics.IsBigO.const_smul_left, MDifferentiable.const_smul, Matrix.row_vecMulVec, SchwartzMap.smulLeftCLM_real_smul, Rep.diagonalSuccIsoFree_inv_hom_single_single, Differentiable.const_smul, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, MeasureTheory.IntegrableAtFilter.smul, PolynomialLaw.smul_def, MeasureTheory.Integrable.smul_enorm, Matrix.smul_vecMul, Matrix.instSMulCommClassForall_1, MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top, fwdDiff_const_smul, DifferentiableAt.const_smul, BoxIntegral.HasIntegral.smul, cross_cross_eq_smul_sub_smul, Matrix.vecMulVec_update, WeierstrassCurve.Projective.addXYZ_of_X_eq, MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc, ZLattice.covolume.tendsto_card_div_pow, Filter.BoundedAtFilter.smul, iteratedFDerivWithin_const_smul_apply, MeasureTheory.Integrable.smul, ContDiffMapSupportedIn.coe_smul, LieModuleHom.coe_smul, smulCommClass, HasFDerivWithinAt.const_smul, Matrix.permanent_updateRow_smul, ContinuousAlternatingMap.coe_smul, ProbabilityTheory.covariance_smul_left, TestFunction.coe_smul, logDeriv_eqOn_iff, cuspFunction_smul, AddConstMap.coe_smul, Matrix.diagonal_smul, MeasureTheory.Submartingale.smul_nonneg, ProbabilityTheory.condVar_smul, Matrix.det_updateRow_sum_aux, Matrix.smul_of, iteratedFDeriv_const_smul_apply, VectorField.lieBracket_const_smul_left, support_const_smul_subset, HasDerivAtFilter.const_smul, VectorFourier.fourierIntegral_const_smul, MeasureTheory.setToFun_smul, LSeries_smul, HahnSeries.SummableFamily.coe_smul', WeierstrassCurve.Projective.negAddY_smul, QuadraticMap.polar_smul, CompactlySupportedContinuousMap.coe_smul, MeasureTheory.AEFinStronglyMeasurable.const_smul, Seminorm.coe_smul, HahnSeries.coeff_smul', Module.Basis.smul_det, NonarchAddGroupSeminorm.coe_smul, iteratedDeriv_const_smul, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.add_of_Z_eq_zero_left, MeasureTheory.Lp.coeFn_smul, CuspForm.coe_smul, iteratedDerivWithin_const_smul_field, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.logMap_real_smul, Finset.weightedVSub_smul, MeasureTheory.Measure.rnDeriv_smul_left', Matrix.permanent_updateCol_smul, MDifferentiableAt.const_smul, DiffContOnCl.const_smul, WeierstrassCurve.Projective.negY_smul, Matrix.vec_smul, Module.Basis.coe_smul, derivWithin_const_smul_field, Finset.centerMass_smul_left, fderivWithin_const_smul_of_field, pi_eq_sum_univ', MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top', WeierstrassCurve.Projective.dblX_smul, InnerProductSpace.laplacian_smul, MeasureTheory.MemLp.const_smul, InnerProductSpace.laplacianWithin_smul, EuclideanHalfSpace.convex, Matrix.det_updateRow_sum, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, IsBoundedLinearMap.smul, WeierstrassCurve.Projective.addXYZ_neg, fourierCoeff.const_smul, WeierstrassCurve.Projective.addZ_smul, LSeriesHasSum.smul, fderiv_const_smul_of_invertible, Matrix.vecMul_eq_sum, NumberField.mixedEmbedding.fundamentalCone.expMap_smul, Matrix.mul_single_eq_updateCol_zero, UniformFun.toFun_smul, AnalyticOn.const_smul, MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq, Measurable.const_smul, fderivWithin_comp_smul_eq_fderivWithin_smul, MeasureTheory.condExp_smul, AffineBasis.det_smul_coords_eq_cramer_coords, MeasureTheory.smul_extend, WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_left, LinearPMap.coe_smul, WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, Fourier.fourierIntegral_const_smul, affineIndependent_smul, gauge_smul_left_of_nonneg, Filter.Germ.coe_smul, Height.mulHeight_smul_eq_mulHeight, HasDerivAt.const_smul, HasFDerivAtFilter.const_smul, MemHolder.smul, ContinuousMapZero.coe_smul, Matrix.vecMul_ofNat, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, extDeriv_smul, EuclideanQuadrant.convex, MeasureTheory.eLpNorm_const_smul_le', Finset.weightedVSub_const_smul, MeasureTheory.Adapted.smul, Matrix.Module.instIsScalarTowerForall, Fin.partialProd_left_inv, Matrix.Module.scalar_smul, WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero, MeasureTheory.Measure.coe_smul, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, MultilinearMap.coe_smul, NumberField.mixedEmbedding.norm_smul, WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_right, MeasureTheory.Integrable.toL1_smul', ContinuousAlternatingMap.hasBasis_nhds_zero, Polynomial.sylvesterDeriv_updateRow, WeierstrassCurve.Projective.smul_fin3, Matrix.mulVec_smul, MeasureTheory.FiniteMeasure.coeFn_smul, WeierstrassCurve.Projective.neg_of_Z_ne_zero, Matrix.smul_vec3, iteratedDerivWithin_const_smul, Finset.weightedVSubOfPoint_smul, MeasureTheory.pdf.IsUniform.pdf_eq, HasFPowerSeriesWithinOnBall.const_smul, fderivWithin_const_smul_of_invertible, UniformFun.ofFun_smul, WeierstrassCurve.Projective.add_of_Z_eq_zero_right, Real.circleAverage_smul, VectorField.lieBracket_const_smul_right, Matrix.blockDiagonal_smul, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, MeasureTheory.uniformIntegrable_average, HasStrictDerivAt.const_smul, MeasureTheory.StronglyAdapted.smul, MeasureTheory.eLpNorm_const_smul_le, support_const_smul_of_ne_zero, MeasureTheory.condLExp_smul_le, WeierstrassCurve.Projective.negDblY_smul, MeasureTheory.SimpleFunc.coe_smul, PolynomialLaw.toFun_smul, LSeriesSummable.smul_iff, Finsupp.coe_smul, HasFDerivAt.const_smul, ContMDiffMap.coe_smul, Matrix.vecMulVec_smul', MeasureTheory.eLpNorm'_const_smul, Tactic.ComputeAsymptotics.Majorized.smul, ContinuousAffineMap.coe_smul, ModularForm.IsGLPos.coe_smul, Matrix.mulVec_eq_sum, IsCompactOperator.smul_unit_iff, DifferentiableWithinAt.const_smul, Derivation.coe_smul, Matrix.single_mul_eq_updateRow_zero, InnerProductSpace.HarmonicOnNhd.const_smul, MeasureTheory.SignedMeasure.rnDeriv_smul, MeasureTheory.Supermartingale.smul_nonpos, Matrix.ofNat_mulVec, dotProduct_smul, translate_smul_right, MeasureTheory.eLpNorm_const_smul, Matrix.vecMul_diagonal_const, pi_eq_sum_univ, WeierstrassCurve.Projective.add_smul_equiv, LeftInvariantDerivation.coe_smul, convex_stdSimplex, ProbabilityTheory.mgf_smul_left, noZeroSMulDivisors, IsCompactOperator.smul_iff₀, HasFPowerSeriesAt.const_smul, RootPairing.GeckConstruction.f_lie_v_ne, derivWithin_const_smul, Matrix.IsHermitian.exists_eigenvector_of_ne_zero, MeasureTheory.lpNorm_const_smul, WeierstrassCurve.Projective.add_smul_of_not_equiv, LSeries.term_smul_apply, Matrix.update_vecMulVec, RootPairing.GeckConstruction.e_lie_v_ne, Matrix.instIsScalarTowerForall, AddGroupSeminorm.coe_smul, AnalyticAt.const_smul, PolynomialLaw.neg_def, fderivWithin_const_smul_field, ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis, Periodic.cuspFunction_smul, WeierstrassCurve.Projective.addU_smul, Matrix.vecMul_natCast, Matrix.replicateCol_smul, Matrix.det_updateCol_smul, MemHolder.nnHolderNorm_smul, BoxIntegral.integralSum_smul, MvPowerSeries.HasSubst.smul, NumberField.mixedEmbedding.convexBodyLT_convex, WeierstrassCurve.Projective.add_of_Y_eq, ProbabilityTheory.covariance_smul_right, AlternatingMap.coeFn_smul, WeierstrassCurve.Projective.equation_smul, WeierstrassCurve.Projective.add_of_X_ne, GroupSeminorm.coe_smul, HasDerivWithinAt.const_smul, MeasureTheory.OuterMeasure.smul_boundedBy, Matrix.mulVec_cramer, LSeries.mul_delta_eq_smul_delta, MeasureTheory.StronglyMeasurable.const_smul, fderivWithin_const_smul, Matrix.instSMulCommClassForall, WeierstrassCurve.Projective.add_of_Y_ne', MeasureTheory.AEEqFun.smul_mk, WeierstrassCurve.Projective.neg_of_Z_eq_zero, WeierstrassCurve.Projective.dblY_smul, FormalMultilinearSeries.ofScalars_smul, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'', Finset.weightedVSubOfPoint_const_smul, NumberField.mixedEmbedding.logMap_real, Seminorm.finset_sup_smul, Matrix.natCast_mulVec, extDerivWithin_smul, MeasureTheory.integrable_smul_iff, IsCompactOperator.smul, CurveIntegrable.smul, BoxIntegral.Integrable.smul, MeasureTheory.HasFiniteIntegral.smul, Pi.single_smul', MeasureTheory.Submartingale.smul_nonpos, Module.Basis.toMatrix_smul_left, Matrix.diagonal_const_mulVec, IsCompactOperator.smul_isUnit_iff, Matrix.vecMulVec_mul_vecMulVec, MeasureTheory.eLpNorm'_const_smul_le, NumberField.mixedEmbedding.normAtPlace_smul, InnerProductSpace.laplacianWithin_smul_nhds, PolynomialLaw.toFun_neg, Polynomial.fwdDiff_iter_degree_eq_factorial, WeierstrassCurve.Projective.neg_smul, MeasureTheory.Measure.rnDeriv_smul_left, ModularForm.prod_fintype_slash, CuspForm.IsGLPos.coe_smul, MeasureTheory.withDensityᵥ_smul, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, iteratedDeriv_const_smul_field, Matrix.cons_vecMulVec, Matrix.cons_vecMul, differentiableWithinAt_smul_iff, DifferentiableOn.const_smul, Matrix.vecMulVec_cons, Matrix.det_updateRow_smul, LSeries.delta_mul_eq_smul_delta, WeierstrassCurve.Projective.add_smul_of_equiv, Matrix.cons_vecMul_cons, Matrix.vecMulVec_mulVec, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, Matrix.Module.diagonal_const_smul, MeasureTheory.condLExp_smul', CentroidHom.coe_smul, Matrix.vecMulVec_smul, deriv_const_smul', MeasureTheory.OuterMeasure.mkMetric_smul, MeasureTheory.eLpNorm'_const_smul_le', MeasureTheory.MemLp.const_smul', Matrix.blockDiag_smul, MeasureTheory.withDensity_smul, LSeries.term_smul, InnerProductSpace.laplacian_smul_nhds, IsUnit.integrable_smul_iff, NumberField.mixedEmbedding.convexBodySum_convex, gauge_smul_left, ProbabilityTheory.variance_smul', Matrix.mulVec_single, IsCompactOperator.smul_iff, Matrix.smul_vec2, Height.logHeight_smul_eq_logHeight, SlashInvariantForm.coe_smul, IntervalIntegrable.smul, NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, TemperedDistribution.smulLeftCLM_smul, VectorField.lieBracketWithin_const_smul_right, Matrix.intCast_mulVec, Filter.ZeroAtFilter.smul, fourierCoeffOn.const_smul, ModularForm.coe_smul, cross_cross_eq_smul_sub_smul', WeierstrassCurve.Projective.smul_fin3_ext, MeasureTheory.Supermartingale.smul_nonneg, WeierstrassCurve.Projective.add_of_Y_ne, ContinuousMap.coe_smul, QuadraticMap.coeFn_smul, HolderWith.smul, NormedAddGroupHom.coe_smul, Matrix.vecMul_cons, Matrix.vecMul_intCast, MeasureTheory.OuterMeasure.mkMetric_nnreal_smul, UniformOnFun.toFun_smul, Matrix.IsHermitian.mulVec_eigenvectorBasis, extend_smul, UniformOnFun.ofFun_smul, Matrix.replicateRow_smul, WeierstrassCurve.Projective.comp_smul, Matrix.mulVec_cons, UniformContinuous.const_smul, MeasureTheory.hasFiniteIntegral_smul_iff, LinearMap.IsAdjointPair.smul, Matrix.vecMul_smul, LinearMap.CompatibleSMul.pi, MeasureTheory.OuterMeasure.smul_ofFunction, fderiv_const_smul_of_field, Even.const_smul, AnalyticOnNhd.const_smul, Measurable.fun_const_smul, qExpansion_smul, eHolderNorm_smul, ZMod.dft_const_smul, MeasureTheory.LocallyIntegrable.smul, fderiv_const_smul, Representation.IntertwiningMap.coe_smul, Odd.const_smul, WeierstrassCurve.Projective.neg_smul_equiv, ProbabilityTheory.variance_smul, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, ConformalAt.const_smul, MeasureTheory.OuterMeasure.coe_smul, deriv_const_smul_field, WeierstrassCurve.Projective.dblXYZ_of_Y_eq, MeasureTheory.MemLp.toLp_const_smul, fwdDiff_iter_const_smul, Matrix.smul_mulVec, MeasureTheory.withDensity_smul', CauSeq.coe_smul, derivWithin_const_smul', WeierstrassCurve.Projective.smul_equiv, SchwartzMap.smulLeftCLM_smul, MemHolder.smul_iff, const_smul_mfderiv, HasMFDerivAt.const_smul, MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top, ModularForm.SL_smul_slash, NumberField.mixedEmbedding.convexBodyLT'_convex, HolderWith.smul_iff, MeasureTheory.eLpNormEssSup_const_smul_le', VectorField.lieBracketWithin_const_smul_left, Asymptotics.IsLittleO.const_smul_left, Matrix.det_smul_inv_vecMul_eq_cramer_transpose, Matrix.smul_mat_empty, WeierstrassCurve.Projective.nonsingular_smul, LinearEquiv.conjAlgEquiv_ext_iff, Matrix.col_vecMulVec, smul_dotProduct, WeierstrassCurve.Projective.dblZ_smul
hasVAdd 📖	CompOp	21 math math: AddConstMap.coe_addLeftHom_apply, AEMeasurable.const_vadd, vaddCommClass, AffineIndependent.vadd, AffineBasis.coe_vadd, Finset.weightedVSubOfPoint_vadd, UniformContinuous.const_vadd, ContinuousMap.coe_vadd, extend_vadd, Measurable.fun_const_vadd, Fin.partialSum_left_neg, Measurable.const_vadd, MeasureTheory.SimpleFunc.coe_vadd, MeasureTheory.AEStronglyMeasurable.const_vadd, Finset.weightedVSub_vadd, Embedding.coe_vadd, Filter.Germ.coe_vadd, AddConstMap.coe_vadd, LocallyConstant.coe_vadd, affineIndependent_vadd, MeasureTheory.StronglyMeasurable.const_vadd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extend_smul 📖	mathematical	—	extend hasSMul	—	extend_def
extend_vadd 📖	mathematical	—	extend HVAdd.hVAdd instHVAdd hasVAdd	—	extend_def
smulCommClass 📖	mathematical	—	SMulCommClass hasSMul	—	Pi.smulCommClass
update_smul 📖	mathematical	—	update Pi.instSMul	—	apply_update
update_vadd 📖	mathematical	—	update HVAdd.hVAdd instHVAdd Pi.instVAdd	—	apply_update
vaddCommClass 📖	mathematical	—	VAddCommClass hasVAdd	—	Pi.vaddCommClass

Pi

Definitions

Name	Category	Theorems
addAction 📖	CompOp	—
addAction' 📖	CompOp	—
mulAction 📖	CompOp	18 math math: WeierstrassCurve.Projective.nonsingularLift_some, WeierstrassCurve.Projective.Point.zero_point, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left, WeierstrassCurve.Projective.smul_eq, classifyingSpaceUniversalCover_map, WeierstrassCurve.Projective.addMap_eq, WeierstrassCurve.Projective.Point.fromAffine_some, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, WeierstrassCurve.Projective.nonsingularLift_iff, WeierstrassCurve.Projective.addMap_of_Y_eq, WeierstrassCurve.Projective.negMap_eq, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right, WeierstrassCurve.Projective.Point.zero_def, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, WeierstrassCurve.Projective.nonsingularLift_zero, classifyingSpaceUniversalCover_obj
mulAction' 📖	CompOp	—
smul' 📖	CompOp	112 math math: smulCommClass', ConvexOn.smul'', MeasureTheory.eLpNorm_smul_le_mul_eLpNorm, derivWithin_smul, MeasureTheory.MemLp.smul, ConcaveOn.mul_convexOn', NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded, Module.Basis.groupSMul_span_eq_top, Function.support_smul_subset_left, smulCommClass'', ConcaveOn.smul_convexOn', ConcaveOn.smul_convexOn, TendstoLocallyUniformly.smul₀, ConcaveOn.smul'', LinearIndependent.group_smul_iff, analyticOrderAt_smul_eq_top_of_left, TendstoLocallyUniformly.smul₀_of_isBoundedUnder, MeasureTheory.Integrable.smul_bdd, DifferentiableAt.smul, meromorphicNFOn_smul_iff_right_of_analyticOnNhd, TendstoLocallyUniformlyOn.smul₀_of_isBoundedUnder, isScalarTower', fderiv_smul, Measurable.smul', HasCompactSupport.smul_left, AnalyticAt.smul, smul_apply', MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, ConvexOn.smul_concaveOn', HasStrictDerivAt.smul, instIsBoundedSMul', Function.support_smul, MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm', Function.support_smul_subset_right, isIsometricSMul', HasCompactSupport.smul_right, LocallyFinite.smul_left, ContDiffWithinAt.smul, Bornology.isVonNBounded_iff_smul_tendsto_zero, fderivWithin_smul, ContinuousMap.coe_smul', MeasureTheory.Integrable.bdd_smul, meromorphicOrderAt_smul, deriv_smul, MeasureTheory.Integrable.smul_of_top_left, ConvexOn.smul_concaveOn, single_smul₀, fwdDiff_smul, Fintype.piFinset_smul, MeasureTheory.Lp.coeFn_lpSMul, analyticAt_iff_analytic_smul, ContDiff.smul, Sym2.lift_smul_lift, MeromorphicAt.meromorphicTrailingCoeffAt_smul, MeasureTheory.Submartingale.sum_smul_sub', smul_def', Function.Even.smul_odd, DifferentiableOn.smul, MeasureTheory.Lp.smul_def, meromorphicOrderAt_smul_of_ne_zero, HasDerivWithinAt.smul, Fintype.piFinset_smul_finset, iteratedDerivWithin_smul, MeromorphicNFAt.smul_analytic, Function.HasTemperateGrowth.smul, LocallyFinite.smul_right, MvPowerSeries.rescale_eq_subst, ContDiffOn.smul, MeromorphicOn.extract_zeros_poles, MvPowerSeries.HasSubst.smul_X, LinearIndependent.units_smul, meromorphicNFAt_smul_iff_right_of_analyticAt, MeromorphicOn.smul, MeasureTheory.Submartingale.sum_smul_sub, MeromorphicOn.divisor_smul, AddAction.automorphize_smul_left, Function.Odd.smul_even, HasFDerivWithinAt.smul, Filter.Germ.coe_smul', Function.Even.smul_even, QuotientGroup.automorphize_smul_left, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, ConcaveOn.smul', LinearIndependent.units_smul_iff, analyticOrderAt_smul, MulAction.automorphize_smul_left, QuotientAddGroup.automorphize_smul_left, TendstoLocallyUniformlyOn.smul₀, Bornology.IsVonNBounded.smul_tendsto_zero, ContDiffAt.smul, LinearIndependent.group_smul, meromorphicAt_smul_iff_of_ne_zero, ConvexOn.smul', IsLinearTopology.tendsto_smul_zero, Function.Odd.smul_odd, QuadraticMap.polarSym2_map_smul, HasDerivAt.smul, Meromorphic.smul, isScalarTower'', Module.Basis.units_smul_span_eq_top, fwdDiff_smul_const, MeromorphicAt.smul, analyticOrderAt_smul_eq_top_of_right, Differentiable.smul, AbsolutelyContinuousOnInterval.smul, DifferentiableWithinAt.smul, HasFDerivAt.smul, MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm, MeasureTheory.Integrable.smul_of_top_right, HasStrictFDerivAt.smul, Module.Basis.groupSMul_apply, MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
vadd' 📖	CompOp	12 math math: Fintype.piFinset_vadd_finset, isIsometricVAdd', Fintype.piFinset_vadd, vadd_def', Filter.Germ.coe_vadd', LipschitzWith.vadd, vaddAssocClass', vaddCommClass'', vaddAssocClass'', vaddCommClass', vadd_apply', Measurable.vadd'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithfulSMul 📖	mathematical	FaithfulSMul	instSMul	—	faithfulSMul_at
faithfulSMul_at 📖	mathematical	—	FaithfulSMul instSMul	—	FaithfulSMul.eq_of_smul_eq_smul Function.update_self
faithfulVAdd 📖	mathematical	FaithfulVAdd	instVAdd	—	faithfulVAdd_at
faithfulVAdd_at 📖	mathematical	—	FaithfulVAdd instVAdd	—	FaithfulVAdd.eq_of_vadd_eq_vadd Function.update_self
isCentralScalar 📖	mathematical	IsCentralScalar	instSMul MulOpposite	—	IsCentralScalar.op_smul_eq_smul
isCentralVAdd 📖	mathematical	IsCentralVAdd	instVAdd AddOpposite	—	IsCentralVAdd.op_vadd_eq_vadd
isScalarTower 📖	mathematical	IsScalarTower	instSMul	—	smul_assoc
isScalarTower' 📖	mathematical	IsScalarTower	instSMul smul'	—	smul_assoc
isScalarTower'' 📖	mathematical	IsScalarTower	smul'	—	smul_assoc
smulCommClass 📖	mathematical	SMulCommClass	instSMul	—	SMulCommClass.smul_comm
smulCommClass' 📖	mathematical	SMulCommClass	instSMul smul'	—	SMulCommClass.smul_comm
smulCommClass'' 📖	mathematical	SMulCommClass	smul'	—	SMulCommClass.smul_comm
smul_apply' 📖	mathematical	—	smul'	—	—
smul_def' 📖	mathematical	—	smul'	—	—
vaddAssocClass 📖	mathematical	VAddAssocClass	instVAdd	—	vadd_assoc
vaddAssocClass' 📖	mathematical	VAddAssocClass	instVAdd vadd'	—	vadd_assoc
vaddAssocClass'' 📖	mathematical	VAddAssocClass	vadd'	—	vadd_assoc
vaddCommClass 📖	mathematical	VAddCommClass	instVAdd	—	VAddCommClass.vadd_comm
vaddCommClass' 📖	mathematical	VAddCommClass	instVAdd vadd'	—	VAddCommClass.vadd_comm
vaddCommClass'' 📖	mathematical	VAddCommClass	vadd'	—	VAddCommClass.vadd_comm
vadd_apply' 📖	mathematical	—	HVAdd.hVAdd instHVAdd vadd'	—	—
vadd_def' 📖	mathematical	—	HVAdd.hVAdd instHVAdd vadd'	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piecewise_smul 📖	mathematical	—	piecewise Pi.instSMul	—	piecewise_op
piecewise_vadd 📖	mathematical	—	piecewise HVAdd.hVAdd instHVAdd Pi.instVAdd	—	piecewise_op

---

← Back to Index