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	457 math math: `AnalyticWithinAt.const_smul`, `ArithmeticFunction.vonMangoldt.residueClass_eq`, `AffineIndependent.smul`, `MeasureTheory.AEEqFun.coeFn_smul`, `NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'`, `IsIntegralCurve.comp_mul`, `Derivative.serreDerivative_smul`, `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`, `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`, `TemperedDistribution.fourierMultiplierCLM_smul`, `AffineBasis.coe_smul`, `stdSimplex_fin_two`, `deriv_const_smul`, `RKHS.coe_smul`, `WeierstrassCurve.Projective.dblU_smul`, `curveIntegralFun_smul`, `ContinuousLinearMap.coe_smul'`, `LSeriesSummable.smul`, `Matrix.submatrix_smul`, `Derivative.normalizedDerivOfComplex_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`, `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`, `isIntegralCurveAt_comp_mul_ne_zero`, `WeierstrassCurve.Projective.dblXYZ_smul`, `Matrix.det_updateRow_add_smul_self`, `differentiableAt_smul_iff`, `HasFPowerSeriesOnBall.const_smul`, `HasStrictFDerivAt.const_smul`, `ProbabilityTheory.HasGaussianLaw.smul`, `extDeriv_fun_smul`, `SlashInvariantForm.coe_smulℝ`, `EisensteinSeries.E2_slash_action`, `IsIntegralCurveOn.comp_mul`, `Filter.TendstoCofinite.mapDomain_smul`, `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`, `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'`, `InnerProductSpace.HarmonicContOnCl.const_smul`, `WeierstrassCurve.Projective.dblX_smul`, `InnerProductSpace.laplacian_smul`, `MeasureTheory.MemLp.const_smul`, `ModularForm.eta_comp_eq_csqrt_I_inv`, `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`, `DiscreteConvolution.ConvolutionExistsAt.smul_convolution`, `LieAlgebra.IsKilling.rootSpace_one_div_two_smul`, `extDeriv_smul`, `EuclideanQuadrant.convex`, `MeasureTheory.eLpNorm_const_smul_le'`, `Finset.weightedVSub_const_smul`, `MeasureTheory.Adapted.smul`, `DiscreteConvolution.ConvolutionExistsAt.convolution_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`, `isIntegralCurveOn_comp_mul_ne_zero`, `MeasureTheory.pdf.IsUniform.pdf_eq`, `HasFPowerSeriesWithinOnBall.const_smul`, `fderivWithin_const_smul_of_invertible`, `UniformFun.ofFun_smul`, `WeierstrassCurve.Projective.add_of_Z_eq_zero_right`, `DiscreteConvolution.AddConvolutionExistsAt.convolution_vadd`, `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`, `IsIntegralCurveAt.comp_mul_ne_zero`, `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`, `DiscreteConvolution.AddConvolutionExistsAt.vadd_convolution`, `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`, `Finsupp.instIsScalarTowerForall`, `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`, `isIntegralCurve_comp_mul_ne_zero`, `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`, `tendsto_card_div_pow_atTop_volume'`, `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`, `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`, `SchwartzMap.fourierMultiplierCLM_smul`, `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	20 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`, `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	22 math math: `WeierstrassCurve.Projective.nonsingularLift_some`, `WeierstrassCurve.Projective.Point.zero_point`, `WeierstrassCurve.Projective.Point.toAffineLift_of_Z_ne_zero`, `WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left`, `WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero`, `WeierstrassCurve.Projective.Point.toAffineLift_some`, `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`, `WeierstrassCurve.Projective.Point.toAffineLift_eq`, `classifyingSpaceUniversalCover_obj`
`mulAction'` 📖	CompOp	—
`smul'` 📖	CompOp	152 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`, `ContMDiffCovariantDerivativeOn.affine_combination`, `VectorField.mpullbackWithin_smul`, `Module.Basis.groupSMul_span_eq_top`, `Function.support_smul_subset_left`, `smulCommClass''`, `VectorField.mlieBracket_smul_left`, `ConcaveOn.smul_convexOn'`, `ConcaveOn.smul_convexOn`, `InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul`, `TendstoLocallyUniformly.smul₀`, `ConcaveOn.smul''`, `LinearIndependent.group_smul_iff`, `analyticOrderAt_smul_eq_top_of_left`, `TendstoLocallyUniformly.smul₀_of_isBoundedUnder`, `MeasureTheory.Integrable.smul_bdd`, `instContinuousSMulForall_1`, `DifferentiableAt.smul`, `HasMFDerivAt.smul`, `fromTangentSpace_mfderiv_smul_apply`, `meromorphicNFOn_smul_iff_right_of_analyticOnNhd`, `MeasureTheory.condExp_smul_of_aestronglyMeasurable_right`, `TendstoLocallyUniformlyOn.smul₀_of_isBoundedUnder`, `isScalarTower'`, `fderiv_smul`, `Finsupp.coe_pointwise_smul`, `Measurable.smul'`, `HasCompactSupport.smul_left`, `AnalyticAt.smul`, `smul_apply'`, `MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt`, `VectorField.mpullback_smul_apply`, `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`, `CovariantDerivative.affine_combination_toFun`, `fromTangentSpace_mfderiv_smul'`, `MDifferentiableAt.smul_section`, `fromTangentSpace_mfderiv_smul_apply'`, `Bornology.isVonNBounded_iff_smul_tendsto_zero`, `fderivWithin_smul`, `ContinuousMap.coe_smul'`, `IsCovariantDerivativeOn.leibniz`, `MeasureTheory.Integrable.bdd_smul`, `VectorField.mlieBracketWithin_smul_left`, `VectorField.mlieBracketWithin_smul_right`, `meromorphicOrderAt_smul`, `deriv_smul`, `VectorField.mpullbackWithin_smul_apply`, `MeasureTheory.Integrable.smul_of_top_left`, `DiffContOnCl.circleAverage_poissonKernel_smul`, `ConvexOn.smul_concaveOn`, `single_smul₀`, `DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul`, `fwdDiff_smul`, `Fintype.piFinset_smul`, `MeasureTheory.Lp.coeFn_lpSMul`, `analyticAt_iff_analytic_smul`, `MeasureTheory.condExp_smul_of_aestronglyMeasurable_left`, `fromTangentSpace_mfderiv_smul`, `ContDiff.smul`, `Sym2.lift_smul_lift`, `MeromorphicAt.meromorphicTrailingCoeffAt_smul`, `MeasureTheory.Submartingale.sum_smul_sub'`, `InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul`, `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`, `VectorField.mpullback_smul`, `InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_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`, `InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul`, `HasFDerivWithinAt.smul`, `Filter.Germ.coe_smul'`, `MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity`, `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`, `mfderiv_smul`, `TendstoLocallyUniformlyOn.smul₀`, `ContMDiffOn.smul_section_of_tsupport`, `ContMDiffWithinAt.smul_section`, `Bornology.IsVonNBounded.smul_tendsto_zero`, `MDifferentiableOn.smul_section`, `ContDiffAt.smul`, `LinearIndependent.group_smul`, `meromorphicAt_smul_iff_of_ne_zero`, `ConvexOn.smul'`, `MDifferentiableOn.smul_section_of_tsupport`, `IsLinearTopology.tendsto_smul_zero`, `Function.Odd.smul_odd`, `mdifferentiable_smul_section`, `QuadraticMap.polarSym2_map_smul`, `IsCovariantDerivativeOn.affine_combination`, `HasDerivAt.smul`, `Meromorphic.smul`, `isScalarTower''`, `Module.Basis.units_smul_span_eq_top`, `fwdDiff_smul_const`, `MeromorphicAt.smul`, `analyticOrderAt_smul_eq_top_of_right`, `ContMDiffAt.smul_section`, `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`, `ContMDiff.smul_section`, `VectorField.mlieBracket_smul_right`, `MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top`, `MDifferentiableWithinAt.smul_section`, `ContMDiffOn.smul_section`, `TensorialAt.smul`
`vadd'` 📖	CompOp	13 math math: `Fintype.piFinset_vadd_finset`, `isIsometricVAdd'`, `Fintype.piFinset_vadd`, `vadd_def'`, `Filter.Germ.coe_vadd'`, `instContinuousVAddForall_1`, `LipschitzWith.vadd`, `vaddAssocClass'`, `vaddCommClass''`, `vaddAssocClass''`, `vaddCommClass'`, `vadd_apply'`, `Measurable.vadd'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithfulSMul` 📖	mathematical	`FaithfulSMul`	`FaithfulSMul` `instSMul`	—	`faithfulSMul_at`
`faithfulSMul_at` 📖	mathematical	—	`FaithfulSMul` `instSMul`	—	`FaithfulSMul.eq_of_smul_eq_smul` `Function.update_self`
`faithfulVAdd` 📖	mathematical	`FaithfulVAdd`	`FaithfulVAdd` `instVAdd`	—	`faithfulVAdd_at`
`faithfulVAdd_at` 📖	mathematical	—	`FaithfulVAdd` `instVAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd` `Function.update_self`
`isCentralScalar` 📖	mathematical	`IsCentralScalar`	`IsCentralScalar` `instSMul` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`isCentralVAdd` 📖	mathematical	`IsCentralVAdd`	`IsCentralVAdd` `instVAdd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`isScalarTower` 📖	mathematical	`IsScalarTower`	`IsScalarTower` `instSMul`	—	`smul_assoc`
`isScalarTower'` 📖	mathematical	`IsScalarTower`	`IsScalarTower` `instSMul` `smul'`	—	`smul_assoc`
`isScalarTower''` 📖	mathematical	`IsScalarTower`	`IsScalarTower` `smul'`	—	`smul_assoc`
`smulCommClass` 📖	mathematical	`SMulCommClass`	`SMulCommClass` `instSMul`	—	`SMulCommClass.smul_comm`
`smulCommClass'` 📖	mathematical	`SMulCommClass`	`SMulCommClass` `instSMul` `smul'`	—	`SMulCommClass.smul_comm`
`smulCommClass''` 📖	mathematical	`SMulCommClass`	`SMulCommClass` `smul'`	—	`SMulCommClass.smul_comm`
`smul_apply'` 📖	mathematical	—	`smul'`	—	—
`smul_def'` 📖	mathematical	—	`smul'`	—	—
`vaddAssocClass` 📖	mathematical	`VAddAssocClass`	`VAddAssocClass` `instVAdd`	—	`vadd_assoc`
`vaddAssocClass'` 📖	mathematical	`VAddAssocClass`	`VAddAssocClass` `instVAdd` `vadd'`	—	`vadd_assoc`
`vaddAssocClass''` 📖	mathematical	`VAddAssocClass`	`VAddAssocClass` `vadd'`	—	`vadd_assoc`
`vaddCommClass` 📖	mathematical	`VAddCommClass`	`VAddCommClass` `instVAdd`	—	`VAddCommClass.vadd_comm`
`vaddCommClass'` 📖	mathematical	`VAddCommClass`	`VAddCommClass` `instVAdd` `vadd'`	—	`VAddCommClass.vadd_comm`
`vaddCommClass''` 📖	mathematical	`VAddCommClass`	`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