ContinuousLinearMap

📁 Source: Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

Statistics

Metric	Count
Definitions arrowCongr, arrowCongrSL, conjContinuousAlgEquiv, ContinuousLinearMap, coprodEquivL, postcomp, precomp, prodL, restrictScalarsL, toBilinForm, toLinearMap₁₂, toSpanSingletonCLE, topologicalSpace, uniformSpace	14
Theorems arrowCongrSL_apply, arrowCongrSL_symm_apply, arrowCongrSL_toLinearEquiv_apply, arrowCongrSL_toLinearEquiv_symm_apply, arrowCongr_apply, arrowCongr_symm, conjContinuousAlgEquiv_apply, conjContinuousAlgEquiv_apply_apply, conjContinuousAlgEquiv_refl, conjContinuousAlgEquiv_trans, symm_conjContinuousAlgEquiv, symm_conjContinuousAlgEquiv_apply_apply, coe_restrictScalarsL, coe_restrict_scalarsL', completeSpace, continuousConstSMul, continuousSMul, continuous_of_continuous_uncurry, continuous_restrictScalars, coprodEquivL_apply_apply, coprodEquivL_symm_apply, eventually_nhds_zero_mapsTo, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, instCompleteSpace, instContinuousEvalConst, instT2Space, isEmbedding_postcomp, isEmbedding_restrictScalars, isInducing_postcomp, isUniformAddGroup, isUniformEmbedding_postcomp, isUniformEmbedding_restrictScalars, isUniformEmbedding_toUniformOnFun, isUniformInducing_postcomp, isVonNBounded_iff, isVonNBounded_image2_apply, map_add₂, map_neg₂, map_smul₂, map_smulₛₗ₂, map_sub₂, map_zero₂, nhds_zero_eq, nhds_zero_eq_of_basis, postcomp_apply, precomp_apply, prodL_apply, toBilinForm_apply, toBilinForm_inj, toBilinForm_injective, toLinearMap₁₂_apply, toLinearMap₁₂_inj, toLinearMap₁₂_injective, toSpanSingletonCLE_apply_apply, toSpanSingletonCLE_symm_apply, toUniformConvergenceCLM_continuous, topologicalAddGroup, uniformContinuousConstSMul, uniformContinuous_restrictScalars	60
Total	74

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
arrowCongr 📖	CompOp	13 math math: MDifferentiableAt.cle_arrowCongr, MDifferentiable.cle_arrowCongr, arrowCongr_apply, MDifferentiableWithinAt.cle_arrowCongr, arrowCongr_symm, ContMDiffOn.cle_arrowCongr, MDifferentiableOn.cle_arrowCongr, fderiv_continuousLinearEquiv_comp, fderivWithin_continuousLinearEquiv_comp, ContMDiffWithinAt.cle_arrowCongr, fderiv_continuousLinearEquiv_comp', ContMDiffAt.cle_arrowCongr, ContMDiff.cle_arrowCongr
arrowCongrSL 📖	CompOp	4 math math: arrowCongrSL_apply, arrowCongrSL_symm_apply, arrowCongrSL_toLinearEquiv_apply, arrowCongrSL_toLinearEquiv_symm_apply
conjContinuousAlgEquiv 📖	CompOp	9 math math: conjContinuousAlgEquiv_refl, conjContinuousAlgEquiv_surjective, conjContinuousAlgEquiv_apply, conjContinuousAlgEquiv_trans, ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv, conjContinuousAlgEquiv_ext_iff, symm_conjContinuousAlgEquiv, conjContinuousAlgEquiv_apply_apply, symm_conjContinuousAlgEquiv_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowCongrSL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap symm	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongrSL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike symm arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongrSL_toLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv ContinuousLinearMap.topologicalSpace IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap symm	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongrSL_toLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquiv ContinuousLinearMap.topologicalSpace IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap symm	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongr_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike ContinuousLinearEquiv RingHomInvPair.ids ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike arrowCongr symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongr_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing arrowCongr	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
conjContinuousAlgEquiv_apply 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousAlgEquiv.equivLike conjContinuousAlgEquiv ContinuousLinearMap.comp RingHomCompTriple.ids toContinuousLinearMap RingHomInvPair.ids symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
conjContinuousAlgEquiv_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike ContinuousAlgEquiv Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousAlgEquiv.equivLike conjContinuousAlgEquiv ContinuousLinearEquiv RingHomInvPair.ids equivLike symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
conjContinuousAlgEquiv_refl 📖	mathematical	—	conjContinuousAlgEquiv refl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousAlgEquiv.refl ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
conjContinuousAlgEquiv_trans 📖	mathematical	—	conjContinuousAlgEquiv trans DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids AddCommGroup.toAddCommMonoid ContinuousAlgEquiv.trans ContinuousLinearMap Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left RingHomCompTriple.ids
symm_conjContinuousAlgEquiv 📖	mathematical	—	ContinuousAlgEquiv.symm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero conjContinuousAlgEquiv symm RingHomInvPair.ids	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
symm_conjContinuousAlgEquiv_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike ContinuousAlgEquiv Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousAlgEquiv.equivLike ContinuousAlgEquiv.symm conjContinuousAlgEquiv ContinuousLinearEquiv RingHomInvPair.ids equivLike symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left

ContinuousLinearMap

Definitions

Name	Category	Theorems
coprodEquivL 📖	CompOp	2 math math: coprodEquivL_apply_apply, coprodEquivL_symm_apply
postcomp 📖	CompOp	10 math math: MDifferentiableOn.clm_postcomp, ContMDiffOn.clm_postcomp, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, MDifferentiable.clm_postcomp, MDifferentiableAt.clm_postcomp, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, postcomp_apply, ContMDiff.clm_postcomp, MDifferentiableWithinAt.clm_postcomp
precomp 📖	CompOp	9 math math: MDifferentiableWithinAt.clm_precomp, ContMDiffOn.clm_precomp, ContMDiffAt.clm_precomp, MDifferentiableAt.clm_precomp, MDifferentiableOn.clm_precomp, MDifferentiable.clm_precomp, ContMDiffWithinAt.clm_precomp, ContMDiff.clm_precomp, precomp_apply
prodL 📖	CompOp	1 math math: prodL_apply
restrictScalarsL 📖	CompOp	4 math math: bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, coe_restrict_scalarsL', coe_restrictScalarsL, bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp
toBilinForm 📖	CompOp	7 math math: ProbabilityTheory.isGaussian_iff_gaussian_charFun, toBilinForm_apply, toBilinForm_inj, ProbabilityTheory.isPosSemidef_covarianceBilin, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, toBilinForm_injective, ProbabilityTheory.isPosSemidef_covarianceBilinDual
toLinearMap₁₂ 📖	CompOp	19 math math: toLinearMap₁₂_injective, toLinearMap₁₂_apply, VectorFourier.fourierIntegral_continuousLinearMap_apply, VectorFourier.hasFDerivAt_fourierIntegral, VectorFourier.fourierIntegral_iteratedFDeriv, VectorFourier.differentiable_fourierIntegral, VectorFourier.iteratedFDeriv_fourierIntegral, toLinearMap₁₂_inj, VectorFourier.fderiv_fourierIntegral, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', VectorFourier.contDiff_fourierIntegral, Real.fourierIntegral_continuousLinearMap_apply', VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, VectorFourier.fourierIntegral_continuousMultilinearMap_apply, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, VectorFourier.fourierIntegral_fderiv, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fourierIntegral_continuousMultilinearMap_apply'
toSpanSingletonCLE 📖	CompOp	2 math math: toSpanSingletonCLE_apply_apply, toSpanSingletonCLE_symm_apply
topologicalSpace 📖	CompOp	681 math math: ContMDiffAt.coordChangeL, instT2Space, MDifferentiable.coordChangeL, ContinuousLinearEquiv.conjContinuousAlgEquiv_refl, LinearMap.mkContinuous₂_norm_le', derivWithin_of_bilinear, Bundle.ContMDiffRiemannianMetric.isVonNBounded, HasDerivWithinAt.clm_comp, topDualPairing_isContPerfPair, LinearMap.mkContinuous₂_apply, isPositive_iff_eq_sum_rankOne, Bundle.ContMDiffRiemannianMetric.contMDiff, continuousOn_stereoToFun, InnerProductSpace.isPositive_rankOne_self, ProbabilityTheory.isGaussian_iff_gaussian_charFun, mulLeftRight_isBoundedBilinear, MDifferentiableOn.clm_postcomp, analyticWithinAt_bilinear, HasCompactSupport.convolution_integrand_bound_left, compSL_apply, continuous₂, Continuous.clm_comp_const, SchwartzMap.integral_sesq_fourier_fourier, Real.hasFDerivAt_fourierChar_neg_bilinear_left, MeasureTheory.convolution_eq_right', MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, InnerProductSpace.rankOne_one_left_eq_innerSL, continuous_det, map_add_add, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, fderivWithin_fderivWithin_eq_of_mem_nhdsWithin, toLinearMap₁₂_injective, MDifferentiableAt.cle_arrowCongr, ProbabilityTheory.covarianceBilinDual_apply', continuousSMul, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, SchwartzMap.pairing_apply_apply, InnerProductSpace.isIdempotentElem_rankOne_self, Differentiable.clm_comp, hasFDerivAt_integral_of_dominated_loc_of_lip_interval, IsCovariantDerivativeOn.difference_apply, ProbabilityTheory.covarianceBilinDual_apply, Real.fderiv_fourierChar_neg_bilinear_right_apply, HasFDerivWithinAt.clm_apply, Continuous.convolution_integrand_fst, iteratedFDerivWithin_succ_eq_comp_right, ContinuousWithinAt.continuousLinearMapCoprod, innerSL_apply_apply, ProbabilityTheory.covarianceBilin_multivariateGaussian, SchwartzMap.integral_bilin_fourierInv_eq, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, ContMDiffWithinAt.mfderivWithin_const, innerSL_apply_comp_of_isSymmetric, Unitization.splitMul_apply, ContMDiffOn.clm_postcomp, toBilinForm_apply, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, ProbabilityTheory.uncenteredCovarianceBilin_apply, mdifferentiableOn_symm_coordChangeL, opNorm_lsmul_apply_le, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, fderiv_clm_comp, SchwartzMap.bilinLeftCLM_apply, fpowerSeriesBilinear_apply_zero, fderiv_continuousAlternatingMap_apply_const, nhds_zero_eq_of_basis, Bundle.RiemannianMetric.isVonNBounded, ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, Differentiable.fderiv_norm_rpow, integrable_of_bilin_of_bdd_left, norm_iteratedFDeriv_le_of_bilinear_of_le_one, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1, isometry_mul_flip, ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective, HasFDerivWithinAt.linear_multilinear_comp, CStarModule.innerSL_apply, hasDerivWithinAt_of_bilinear, Bundle.ContinuousLinearMap.vectorBundle, contDiff_one_iff_fderiv, MeasureTheory.ConvolutionExistsAt.integrable, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, opNorm_mul_flip_apply, bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, InnerProductSpace.inner_left_rankOne_apply, HasFDerivAt.norm_sq, hasBasis_nhds_zero, Continuous.clm_comp, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, ContDiffAt.continuousAt_fderiv, Real.integrable_prod_sub, topologicalAddGroup, HasFDerivAt.continuousMultilinear_apply_const, InnerProductSpace.rankOne_apply, HasStrictDerivAt.clm_comp, NormedSpace.Dual.toWeakDual_continuous, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMultilinearMap.norm_smulRightL_le, derivWithin_clm_comp, precompL_apply, Bundle.Pretrivialization.continuousLinearMap_apply, VectorBundleCore.contMDiffOn_coordChange, MDifferentiable.clm_postcomp, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, toSesqForm_apply_coe, SchwartzMap.integral_bilin_fourierIntegral_eq, toLinearMap₁₂_apply, NormedSpace.isClosed_polar, VectorFourier.fourierPowSMulRight_eq_comp, hasFDerivWithinAt_of_bilinear, opNorm_mul, MDifferentiable.cle_arrowCongr, flipMultilinear_apply_apply, fderiv_continuousAlternatingMapCompContinuousLinearMap, compactOperator_topologicalClosure, isEmbedding_postcomp, SchwartzMap.integral_sesq_fourier_eq, adjointAux_norm, MDifferentiable.clm_bundle_apply₂, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, ProbabilityTheory.covarianceBilin_apply_basisFun_self, hasStrictFDerivAt_of_bilinear, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, LinearMap.toContinuousBilinearMap_apply, Real.fourier_iteratedFDeriv, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable, MDifferentiableAt.clm_prodMap, mulLeftRight_apply, Bundle.ContinuousRiemannianMetric.symm, ContinuousMultilinearMap.curryRight_norm, analyticOn_bilinear, continuous_of_continuous_uncurry, MDifferentiableAt.clm_postcomp, coe_innerSL_apply, RegularNormedAlgebra.isometry_mul', IsCovariantDerivativeOn.torsion_self, MDifferentiableWithinAt.clm_bundle_apply₂, HasFDerivAt.clm_apply, hasFDerivAt_ringInverse, contDiffAt_one_iff, VectorFourier.fourierIntegral_iteratedFDeriv, InnerProductSpace.nnnorm_rankOne, ContinuousLinearEquiv.arrowCongr_apply, flip_smul, InnerProductSpace.isSymmetricProjection_rankOne_self, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, MeasureTheory.ConvolutionExistsAt.integrable_swap, ContinuousOn.clm_comp, continuousOn_tangentCoordChange, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, instLocallyConvexSpace, NormedSpace.inclusionInDoubleDual_norm_eq, ContinuousLinearEquiv.conjContinuousAlgEquiv_trans, fderiv_of_bilinear, tendsto_integral_exp_smul_cocompact, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, CovariantDerivative.torsion_apply, IsCovariantDerivativeOn.torsion_antisymm, opNorm_mul_apply, norm_smulRightL, NormedSpace.inclusionInDoubleDualWeak_apply_apply, MeasureTheory.convolution_def, ContMDiffFiberwiseLinear.locality_aux₂, compContinuousMultilinearMapL_apply, InnerProductSpace.trace_rankOne, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, ContMDiffVectorBundle.continuousLinearMap, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, continuous_restrictScalars, hasFDerivAt_norm_rpow, compL_apply, lsmul_flip_inj, summable_jacobiTheta₂_term_fderiv_iff, ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM, NormedSpace.toLinearMap_inclusionInDoubleDualWeak, inCoordinates_apply_eq₂, flip_apply, ProbabilityTheory.covarianceBilin_zero, contDiffOn_stereoToFun, fderiv_inverse, ContMDiffOn.clm_precomp, bilinearRestrictScalars_apply_apply, InnerProductSpace.adjoint_rankOne, InnerProductSpace.rankOne_eq_zero, Real.fourierIntegral_convergent_iff', Bundle.ContMDiffRiemannianMetric.symm, ContMDiffOn.coordChangeL, InnerProductSpace.inner_right_rankOne_apply, SchwartzMap.pairing_apply, ContDiff.continuous_fderiv, mdifferentiableAt_hom_bundle, innerSL_inj, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_inv', MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, StrongDual.toLp_of_not_memLp, fderivWithin_of_bilinear, ContinuousWithinAt.clm_comp, NormedSpace.inclusionInDoubleDual_norm_le, Convex.second_derivative_within_at_symmetric, InnerProductSpace.rankOne_eq_rankOne_iff_comm, precompR_apply, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd', ProbabilityTheory.IsGaussian.charFun_eq', ProbabilityTheory.covarianceBilinDual_eq_covariance, ContMDiffAt.mfderiv_const, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ProbabilityTheory.covarianceBilinDual_zero, Continuous.fderiv, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, Bundle.Pretrivialization.continuousLinearMap.isLinear, hasStrictDerivAt_of_bilinear, ContinuousLinearEquiv.arrowCongr_symm, isBoundedBilinearMap, fderivWithin_continuousMultilinear_apply_const, Differentiable.fderiv_two, instContinuousEvalConst, MDifferentiableOn.coordChangeL, continuousMultilinearCurryRightEquiv_symm_apply, lsmul_apply, Bundle.ContMDiffRiemannianMetric.pos, bilinearComp_zero_right, IsContMDiffRiemannianBundle.exists_contMDiff, InnerProductSpace.rank_rankOne, ContMDiffOn.cle_arrowCongr, Convex.taylor_approx_two_segment, MDifferentiableOn.clm_prodMap, contMDiffAt_coordChangeL, adjointAux_apply, ProperCone.innerDual_singleton, hasFDerivAt_integral_of_dominated_loc_of_lip', InnerProductSpace.rankOne_def, MDifferentiableWithinAt.coordChangeL, coe_flipₗᵢ', MDifferentiableAt.clm_bundle_apply₂, stereoToFun_apply, adjointAux_inner_left, hasSum_jacobiTheta₂_term_fderiv, fderivWithin_fderivWithin_eq_of_mem_nhds, ProbabilityTheory.covarianceBilin_comm, SchwartzMap.integral_bilin_fourier_eq, DifferentiableOn.clm_comp, ClosedSubmodule.orthogonal_eq_inter, ContinuousOn.clm_bundle_apply₂, coe_flipMultilinearEquiv, NonUnitalAlgHom.coe_Lmul, ContinuousMultilinearMap.norm_map_init_le, SchwartzMap.smulRightCLM_apply_apply, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin, ContDiffWithinAt.continuousWithinAt_fderivWithin, coe_restrict_scalarsL', fderivWithin_fderivWithin_eq_of_eventuallyEq, ContMDiffOn.clm_comp, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, norm_iteratedFDeriv_le_of_bilinear, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, aestronglyMeasurable_comp₂, HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt, norm_precompR_le, hasFPowerSeriesOnBall_bilinear, eventually_nhds_zero_mapsTo, Convex.isLittleO_alternate_sum_square, deriv_of_bilinear, Orientation.areaForm'_apply, innerSLFlip_apply_apply, nnnorm_holder_apply_apply_le, Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange, bilinear_hasTemperateGrowth, IsContinuousRiemannianBundle.exists_continuous, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, postcomp_apply, prodMapL_apply, ContinuousLinearEquiv.nhds, IsBilinearMap.toContinuousBilinearMap_apply, contMDiffOn_continuousLinearMapCoordChange, InnerProductSpace.enorm_rankOne, InnerProductSpace.continuousLinearMapOfBilin_zero, ContinuousMultilinearMap.compContinuousLinearMapLRight_apply, toLinearMap_innerSL_apply, ContinuousMultilinearMap.flipLinear_apply_apply, Real.fourier_fderiv, Continuous.continuousLinearMapCoprod, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, HasFDerivWithinAt.norm_sq, MDifferentiableAt.clm_comp, HasDerivAt.clm_comp, uncurryBilinear_apply, VectorBundle.continuousOn_coordChange', MeasureTheory.integral_posConvolution, VectorFourier.integral_fourierIntegral_swap, NormedSpace.inclusionInDoubleDualWeak_apply, Bundle.RiemannianMetric.symm, Unitization.norm_eq_sup, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff, iteratedFDerivWithin_two_apply', Bundle.Pretrivialization.continuousLinearMap_symm_apply, memLp_of_bilin, ProbabilityTheory.covarianceBilin_self_nonneg, HasStrictFDerivAt.continuousMultilinear_apply_const, opNorm_mulLeftRight_apply_le, analyticOnNhd_bilinear, ProbabilityTheory.covarianceBilinDual_self_eq_variance, hasStrictFDerivAt_norm_sq, fderiv_tsum, ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, map_sub₂, bilinearComp_apply, ContMDiffWithinAt.clm_bundle_apply₂, tendsto_integral_exp_smul_cocompact_of_inner_product, ContinuousOn.prod_mapL, contMDiffOn_symm_coordChangeL, contMDiffAt_hom_bundle, ContinuousAt.continuousLinearMapCoprod, HasFDerivAt.continuousAlternatingMap_apply_const, ProbabilityTheory.covarianceBilinDual_self_nonneg, ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply, adjointAux_adjointAux, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ContMDiffAt.clm_precomp, ProbabilityTheory.covarianceBilin_real_self, coprodEquivL_apply_apply, flip_add, MDifferentiable.clm_prodMap, continuous_clm_apply, VectorFourier.fourierSMulRight_apply, ContinuousMultilinearMap.uncurryRight_apply, isVonNBounded_iff, bilinearComp_zero, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, Real.fourier_bilin_convolution_eq, hom_trivializationAt, le_opNorm₂, lpPairing_eq_integral, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, InnerProductSpace.rankOne_def', opNorm_mul_le, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, ContDiffOn.continuousOn_fderivWithin, SchwartzMap.integral_sesq_fourierIntegral_eq, MeasureTheory.Integrable.convolution_integrand, ProbabilityTheory.covarianceBilin_apply_pi, SchwartzMap.integral_bilinear_laplacian_right_eq_left, isometry_mul, isOpen_injective, MeasureTheory.dist_convolution_le', isInducing_postcomp, Continuous.prod_map_equivL, CovariantDerivative.torsion_eq_zero_iff, DifferentiableWithinAt.clm_comp, MDifferentiableOn.cle_arrowCongr, InnerProductSpace.innerSL_norm, ContMDiff.clm_bundle_apply₂, second_derivative_symmetric, ContinuousMultilinearMap.curryRight_apply, ContMDiffWithinAt.mfderivWithin, Bundle.Trivialization.baseSet_continuousLinearMap, VectorPrebundle.exists_coordChange, MDifferentiableAt.clm_precomp, ProbabilityTheory.covarianceBilin_apply_basisFun, ContinuousMultilinearMap.analyticOn_uncurry_of_linear, mdifferentiableOn_continuousLinearMapCoordChange, InnerProductSpace.isStarProjection_rankOne_self, LinearMap.mkContinuous₂_norm_le, MeasureTheory.AEStronglyMeasurable.fourierSMulRight, hasFPowerSeriesAt_bilinear, continuousConstSMul, PiTensorProduct.mapLMultilinear_apply_apply, HasFDerivWithinAt.clm_comp, evalL_apply, hasStrictFDerivAt_ringInverse, Continuous.const_clm_comp, ContDiffOn.continuousOn_fderiv_of_isOpen, mul_apply', InnerProductSpace.rankOne_comp_rankOne, InnerProductSpace.rankOne_comp, hasBasis_nhds_zero_of_basis, Real.fourierIntegral_fderiv, InnerProductSpace.toMatrix_rankOne, MDifferentiableWithinAt.clm_comp, HasFDerivWithinAt.continuousMultilinear_apply_const, MDifferentiableOn.clm_comp, InnerProductSpace.isSymmetric_rankOne_self, ContMDiffAt.clm_prodMap, opNNNorm_mul, norm_iteratedFDerivWithin_le_of_bilinear, iteratedFDeriv_succ_eq_comp_right, DifferentiableAt.clm_comp, fderiv_continuousLinearEquiv_comp, deriv_clm_comp, adjoint_toSpanSingleton, toBilinForm_injective, ProbabilityTheory.isPosSemidef_covarianceBilinDual, isEmbedding_restrictScalars, spectrum.hasFDerivAt_resolvent, Bundle.Trivialization.continuousLinearMap_apply, IsBoundedBilinearMap.toContinuousLinearMap_apply, hom_trivializationAt_source, IsCovariantDerivativeOn.add_one_form, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, innerSLFlip_apply, ContinuousAt.clm_bundle_apply₂, ProbabilityTheory.covarianceBilin_real, fderiv_continuousMultilinearMapCompContinuousLinearMap, mdifferentiableOn_coordChangeL, opNorm_mulLeftRight_apply_apply_le, opNorm_lsmul_le, ProbabilityTheory.covarianceBilin_of_not_memLp, innerSL_apply_norm, Real.fourier_bilin_convolution_eq_integral, ContinuousWithinAt.clm_bundle_apply₂, coe_restrictScalarsL, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, norm_compL_le, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, ContMDiffVectorBundle.contMDiffOn_coordChangeL, fderivWithin_clm_comp, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, fderiv_continuousMultilinear_apply_const, ProbabilityTheory.covarianceBilinDual_comm, NormedSpace.isEmbedding_inclusionInDoubleDualWeak, opNNNorm_mul_flip_apply, CovariantDerivative.torsion_antisymm, ContMDiff.clm_postcomp, MDifferentiableAt.coordChangeL, fderivWithin_continuousAlternatingMap_apply_const, ContinuousLinearEquiv.arrowCongrSL_apply, MDifferentiableWithinAt.clm_postcomp, hasFDerivAt_uncurry_of_multilinear, ContMDiff.clm_prodMap, opNorm_mul_apply_le, contDiff_one_iff_hasFDerivAt, ProbabilityTheory.covarianceBilin_apply, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, MeasureTheory.convolutionExistsAt_iff_integrable_swap, hasFDerivAt_tsum, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, norm_bilinearRestrictScalars, nhds_zero_eq, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, ProbabilityTheory.covarianceBilin_map, Unitization.nnnorm_eq_sup, bilinearComp_zero_left, Bundle.ContinuousRiemannianMetric.pos, IsCoercive.continuousLinearEquivOfBilin_apply, VectorBundleCore.continuousOn_coordChange, MDifferentiableOn.clm_precomp, VectorFourier.integral_bilin_fourierIntegral_eq_flip, deriv_clm_apply, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, InnerProductSpace.toLinearMap_rankOne, instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional, adjointAux_inner_right, Bundle.RiemannianMetric.pos, ContinuousLinearEquiv.isOpen, HasStrictFDerivAt.clm_apply, ContMDiffAt.clm_bundle_apply₂, continuousMultilinearCurryRightEquiv_symm_apply', ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, prodL_apply, iteratedFDerivWithin_two_apply, DoubleCentralizer.coe_fst, hasFDerivAt_of_bilinear, ProbabilityTheory.uncenteredCovarianceBilin_zero, TensorialAt.mkHom₂_apply, VectorFourier.fourierPowSMulRight_apply, opNorm_flip, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, VectorPrebundle.continuousOn_coordChange, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub, tendsto_of_tendsto_pointwise_of_cauchySeq, ContMDiffCovariantDerivativeOn.contMDiff, FormalMultilinearSeries.derivSeries_eq_zero, ContMDiffWithinAt.coordChangeL, norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, fderiv_clm_apply, norm_compSL_le, ContMDiffFiberwiseLinear.locality_aux₁, innerSL_apply, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, InnerProductSpace.isIdempotentElem_rankOne_self_iff, fderivWithin_continuousLinearEquiv_comp, StrongDual.toLp_apply, map_smul₂, coe_flipₗᵢ, ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, ContMDiffAt.mfderiv, Continuous.clm_bundle_apply₂, continuousAt_hom_bundle, VectorPrebundle.contMDiffOn_contMDiffCoordChange, IsCovariantDerivativeOn.torsion_apply_eq_extend, Real.differentiable_fourierChar_neg_bilinear_right, OrthonormalBasis.sum_rankOne_eq_id, mdifferentiableAt_coordChangeL, HasStrictFDerivAt.continuousAlternatingMap_apply_const, MeasureTheory.condExp_bilin_of_stronglyMeasurable_right, CovariantDerivative.torsion_self, norm_smulRightL_le, coe_symm_flipMultilinearEquiv, Bundle.Pretrivialization.continuousLinearMap_symm_apply', VectorFourier.norm_fourierSMulRight_le, continuousWithinAt_hom_bundle, le_of_opNorm₂_le_of_le, signedDist_apply, continuousMultilinearCurryRightEquiv_apply', flipₗᵢ'_symm, flip_zero, ContMDiffWithinAt.clm_prodMap, ContinuousAt.clm_comp, VectorFourier.norm_fourierPowSMulRight_le, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, Real.hasFDerivAt_fourierChar_neg_bilinear_right, VectorFourier.norm_fourierSMulRight, hom_chart, toUniformConvergenceCLM_continuous, hasStrictFDerivAt_inv', iteratedFDeriv_two_apply, hom_trivializationAt_apply, MDifferentiable.clm_precomp, MDifferentiable.clm_comp, Real.differentiable_fourierChar_neg_bilinear_left, ContMDiff.clm_comp, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, ContinuousMultilinearMap.smulRightL_apply, instBorelSpace, Convex.second_derivative_within_at_symmetric_of_mem_interior, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, CovariantDerivative.torsion_apply_eq_extend, contMDiffOn_coordChangeL, ContinuousLinearEquiv.arrowCongrSL_symm_apply, opNorm_mulLeftRight_le, ContMDiffWithinAt.clm_precomp, MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound, hom_trivializationAt_baseSet, Submodule.orthogonal_eq_inter, lsmul_flip_apply, compContinuousAlternatingMapCLM_apply_apply, fderiv_norm_rpow, map_add₂, MeasureTheory.integral_bilinear_hasDerivAt_eq_sub, ContMDiff.clm_precomp, Bundle.ContinuousLinearMap.memTrivializationAtlas, ContMDiffOn.clm_prodMap, FormalMultilinearSeries.derivSeries_apply_diag, ContMDiffWithinAt.clm_comp, opNorm_lsmul, ProbabilityTheory.covarianceBilinDual_of_not_memLp, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv, integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable, InnerProductSpace.continuousLinearMapOfBilin_apply, NormedSpace.double_dual_bound, MeasureTheory.convolution_eq_swap, map_zero₂, Real.zero_at_infty_vector_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, precomp_apply, norm_holderL_le, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound, analyticAt_bilinear, ProbabilityTheory.IsGaussian.charFunDual_eq', toPointwiseConvergenceCLM_apply, IsCovariantDerivativeOn.torsion_apply, innerSL_apply_coe, bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, integral_bilinear_fderiv_right_eq_neg_left_of_integrable, hasFDerivAt_inv', exists_continuousLinearEquiv_fderiv_symm_eq, TensorialAt.mkHom₂_apply_eq_extend, MeasureTheory.AEStronglyMeasurable.convolution_integrand', map_neg₂, Bundle.RiemannianMetric.continuousAt, holderL_apply_apply, MeasureTheory.AEStronglyMeasurable.convolution_integrand, norm_innerSL_le, VectorFourier.hasFDerivAt_fourierChar_smul, ContMDiffWithinAt.cle_arrowCongr, continuousMultilinearCurryRightEquiv_apply, integrable_of_bilin_of_bdd_right, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply, apply_apply', ProbabilityTheory.covarianceBilinDual_of_not_memLp', ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, flipₗᵢ_symm, fderivWithin_clm_apply, exists_continuousLinearEquiv_fderivWithin_symm_eq, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, norm_holder_apply_apply_le, ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, HasStrictFDerivAt.clm_comp, VectorFourier.fourierIntegral_fderiv, fderiv_continuousLinearEquiv_comp', smulRightL_apply_apply, continuousOn_clm_apply, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, toSpanSingletonCLE_apply_apply, MDifferentiableWithinAt.clm_prodMap, ContMDiffAt.clm_comp, opNNNorm_mul_apply, toSpanSingletonCLE_symm_apply, mdifferentiableWithinAt_hom_bundle, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, Real.fderiv_fourierChar_neg_bilinear_left_apply, apply_apply, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply, IsSymmSndFDerivWithinAt.eq, map_smulₛₗ₂, PiTensorProduct.mapLMultilinear_opNorm, hasFDerivAt_tsum_of_isPreconnected, Real.fourierIntegral_iteratedFDeriv, derivWithin_clm_apply, hom_trivializationAt_target, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd, HasCompactSupport.convolution_integrand_bound_right, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply, InnerProductSpace.symm_toEuclideanLin_rankOne, ContinuousOn.continuousLinearMapCoprod, ContMDiffAt.cle_arrowCongr, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, HasFDerivAt.clm_comp, adjoint_innerSL_apply, Bundle.Pretrivialization.continuousLinearMapCoordChange_apply, fderiv_tsum_apply, coprodEquivL_symm_apply, ContinuousOn.prod_map_equivL, continuousOn_coordChange, HasCompactSupport.convolution_integrand_bound_right_of_subset, second_derivative_symmetric_of_eventually_of_real, contMDiffWithinAt_hom_bundle, mem_contMDiffFiberwiseLinear_iff, norm_smulRightL_apply, isOpen_setOf_nat_le_rank, isClosed_setOf_isCompactOperator, DoubleCentralizer.coe_snd, opNorm_le_bound₂, fpowerSeriesBilinear_apply_one, MeasureTheory.integral_convolution, fderiv_norm_sq_apply, NormedSpace.dual_def, fderiv_norm_sq, coe_mulₗᵢ, MDifferentiableOn.clm_bundle_apply₂, HasFDerivWithinAt.continuousAlternatingMap_apply_const, innerSL_apply_comp, toSesqForm_apply_norm_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd, coeFn_holder, ContMDiff.cle_arrowCongr, coe_deriv₂, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply, ContMDiffOn.clm_bundle_apply₂, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply, Continuous.prod_mapL, Bundle.ContinuousRiemannianMetric.isVonNBounded, hasDerivAt_of_bilinear, second_derivative_symmetric_of_eventually, ContMDiff.coordChangeL, InnerProductSpace.norm_rankOne, hasFDerivAt_integral_of_dominated_loc_of_lip, PiTensorProduct.mapLMultilinear_toFun_apply, ContinuousMultilinearMap.uncurryRight_norm, flipAlternating_apply_apply, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable, IsSymmSndFDerivAt.eq, norm_iteratedFDerivWithin_le_of_bilinear_aux, fderiv_inv', Continuous.fderiv_one
uniformSpace 📖	CompOp	13 math math: isUniformEmbedding_restrictScalars, completeSpace, uniformContinuous_restrictScalars, isUniformAddGroup, uniformContinuousConstSMul, isUniformInducing_postcomp, instCompleteSpace, SeparatingDual.completeSpace_continuousLinearMap_iff, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology, isUniformEmbedding_postcomp, isUniformEmbedding_toUniformOnFun, UniformCauchySeqOnFilter.one_smulRight, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_restrictScalarsL 📖	mathematical	—	toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module restrictScalarsL restrictScalarsₗ LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsTopologicalAddGroup.toContinuousAdd
coe_restrict_scalarsL' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module funLike restrictScalarsL restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsTopologicalAddGroup.toContinuousAdd
completeSpace 📖	mathematical	Topology.IsCoherentWith setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CompleteSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace	—	UniformConvergenceCLM.completeSpace Bornology.sUnion_isVonNBounded_eq_univ
continuousConstSMul 📖	mathematical	—	ContinuousConstSMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace instSMul DistribMulAction.toDistribSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	UniformConvergenceCLM.instContinuousConstSMul
continuousSMul 📖	mathematical	—	ContinuousSMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass topologicalSpace	—	UniformConvergenceCLM.continuousSMul
continuous_of_continuous_uncurry 📖	mathematical	Continuous instTopologicalSpaceProd DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid funLike LinearMap addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike	Continuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid topologicalSpace DFunLike.coe LinearMap addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformConvergenceCLM.continuous_of_continuous_uncurry
continuous_restrictScalars 📖	mathematical	—	Continuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid topologicalSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	Topology.IsEmbedding.continuous LinearMap.IsScalarTower.compatibleSMul isEmbedding_restrictScalars
coprodEquivL_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule funLike ContinuousLinearEquiv RingHomInvPair.ids topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup Prod.instAddCommGroup module EquivLike.toFunLike ContinuousLinearEquiv.equivLike coprodEquivL AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd
coprodEquivL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule topologicalSpace Prod.instAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm coprodEquivL comp inl inr	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd
eventually_nhds_zero_mapsTo 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Filter Filter.instMembership nhds	Filter.Eventually ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set.MapsTo DFunLike.coe funLike nhds topologicalSpace zero	—	UniformConvergenceCLM.eventually_nhds_zero_mapsTo
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set nhds topologicalSpace zero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter Filter.instMembership setOf	—	hasBasis_nhds_zero_of_basis Filter.basis_sets
hasBasis_nhds_zero_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.HasBasis ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set nhds topologicalSpace zero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid setOf	—	UniformConvergenceCLM.hasBasis_nhds_zero_of_basis Bornology.isVonNBounded_empty directedOn_of_sup_mem Bornology.IsVonNBounded.union
instCompleteSpace 📖	mathematical	—	CompleteSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace	—	completeSpace Topology.IsCoherentWith.of_seq Bornology.IsVonNBounded.insert Filter.Tendsto.isVonNBounded_range
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace	—	UniformConvergenceCLM.continuousEvalConst Bornology.sUnion_isVonNBounded_eq_univ
instT2Space 📖	mathematical	—	T2Space ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace	—	UniformConvergenceCLM.t2Space Bornology.sUnion_isVonNBounded_eq_univ
isEmbedding_postcomp 📖	mathematical	Topology.IsEmbedding DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	Topology.IsEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace comp	—	isInducing_postcomp Topology.IsEmbedding.isInducing cancel_left Topology.IsEmbedding.injective
isEmbedding_restrictScalars 📖	mathematical	—	Topology.IsEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid topologicalSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsUniformEmbedding.isEmbedding isUniformAddGroup_of_addCommGroup LinearMap.IsScalarTower.compatibleSMul isUniformEmbedding_restrictScalars
isInducing_postcomp 📖	mathematical	Topology.IsInducing DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	Topology.IsInducing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace comp	—	IsUniformInducing.isInducing isUniformAddGroup_of_addCommGroup isUniformInducing_postcomp AddMonoidHom.isUniformInducing_of_isInducing DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
isUniformAddGroup 📖	mathematical	—	IsUniformAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace AddCommGroup.toAddGroup addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing IsUniformAddGroup.to_topologicalAddGroup	—	UniformConvergenceCLM.instIsUniformAddGroup
isUniformEmbedding_postcomp 📖	mathematical	IsUniformEmbedding DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid funLike	IsUniformEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace comp	—	UniformConvergenceCLM.isUniformEmbedding_postcomp
isUniformEmbedding_restrictScalars 📖	mathematical	—	IsUniformEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	LinearMap.IsScalarTower.compatibleSMul IsUniformEmbedding.of_comp_iff isUniformEmbedding_toUniformOnFun Bornology.IsVonNBounded.extend_scalars Bornology.IsVonNBounded.restrict_scalars
isUniformEmbedding_toUniformOnFun 📖	mathematical	—	IsUniformEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid uniformSpace UniformOnFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun funLike	—	UniformConvergenceCLM.isUniformEmbedding_coeFn
isUniformInducing_postcomp 📖	mathematical	IsUniformInducing DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid funLike	IsUniformInducing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace comp	—	UniformConvergenceCLM.isUniformInducing_postcomp
isVonNBounded_iff 📖	mathematical	—	Bornology.IsVonNBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction zero topologicalSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image2 DFunLike.coe funLike	—	UniformConvergenceCLM.isVonNBounded_iff
isVonNBounded_image2_apply 📖	mathematical	Bornology.IsVonNBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup zero topologicalSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Bornology.IsVonNBounded SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image2 ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid DFunLike.coe funLike	—	UniformConvergenceCLM.isVonNBounded_image2_apply
map_add₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_add add_apply
map_neg₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass neg_apply
map_smul₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike RingHom.id Semiring.toNonAssocSemiring topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_smul smul_apply
map_smulₛₗ₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_smulₛₗ smul_apply
map_sub₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass sub_apply
map_zero₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_zero zero_apply
nhds_zero_eq 📖	mathematical	—	nhds ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace zero iInf Filter Set Filter.instInfSet Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.instMembership Filter.principal setOf Set.MapsTo DFunLike.coe funLike	—	UniformConvergenceCLM.nhds_zero_eq
nhds_zero_eq_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	nhds ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace zero iInf Filter Set Filter.instInfSet Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.principal setOf Set.MapsTo DFunLike.coe funLike	—	UniformConvergenceCLM.nhds_zero_eq_of_basis
postcomp_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike postcomp comp	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
precomp_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike precomp comp	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
prodL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpaceProd topologicalSpace Prod.instAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup Prod.instModule Prod.instAddCommGroup Prod.instIsTopologicalAddGroup Prod.continuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid module Prod.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction Module.toDistribMulAction Prod.continuousConstSMul EquivLike.toFunLike ContinuousLinearEquiv.equivLike prodL prod	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd Prod.instIsTopologicalAddGroup Prod.continuousAdd Prod.smulCommClass Prod.continuousConstSMul
toBilinForm_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module toBilinForm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace funLike topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing module Algebra.to_smulCommClass Algebra.id SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul
toBilinForm_inj 📖	mathematical	—	toBilinForm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul toBilinForm_injective
toBilinForm_injective 📖	mathematical	—	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.BilinForm toBilinForm	—	toLinearMap₁₂_injective
toLinearMap₁₂_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing toLinearMap₁₂ ContinuousLinearMap funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
toLinearMap₁₂_inj 📖	mathematical	—	toLinearMap₁₂	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self toLinearMap₁₂_injective
toLinearMap₁₂_injective 📖	mathematical	—	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap LinearMap.addCommMonoid LinearMap.module toLinearMap₁₂	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
toSpanSingletonCLE_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Semiring.toModule funLike ContinuousLinearEquiv RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace topologicalSpace NormedAddCommGroup.toAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousLinearEquiv.equivLike toSpanSingletonCLE	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul
toSpanSingletonCLE_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddCommGroup.toAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace topologicalSpace NormedAddCommGroup.toAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm toSpanSingletonCLE NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul
toUniformConvergenceCLM_continuous 📖	mathematical	Set Set.instHasSubset setOf Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Continuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformConvergenceCLM topologicalSpace UniformConvergenceCLM.instTopologicalSpace DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformConvergenceCLM.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toUniformConvergenceCLM	—	continuous_id_of_le UniformConvergenceCLM.topologicalSpace_mono
topologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace AddCommGroup.toAddGroup addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing	—	UniformConvergenceCLM.instIsTopologicalAddGroup
uniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace instSMul DistribMulAction.toDistribSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass	—	UniformConvergenceCLM.instUniformContinuousConstSMul
uniformContinuous_restrictScalars 📖	mathematical	—	UniformContinuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsUniformInducing.uniformContinuous LinearMap.IsScalarTower.compatibleSMul IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_restrictScalars

(root)

Definitions

Name	Category	Theorems
ContinuousLinearMap 📖	CompData	3169 math math: Polynomial.fderiv, Matrix.l2_opNorm_toEuclideanCLM, IsLocalMaxOn.fderivWithin_nonpos, LinearMap.det_toContinuousLinearMap, MeasureTheory.L1.setToL1_eq_setToL1', TangentBundle.continuousLinearMapAt_model_space, hasFDerivAt_iff_hasDerivAt, TestFunction.lineDerivCLM_apply_of_le, ContinuousLinearEquiv.antilipschitz, VectorBundleCore.toFiberBundleCore_coordChange, ContMDiffAt.coordChangeL, ContinuousOn.clm_apply, LinearMap.IsSymmetric.clm_adjoint_eq, mfderiv_prod_eq_add, ContinuousMap.toLp_inj, TopModuleCat.hom_cokerπ, ContinuousLinearMap.comp_neg, TemperedDistribution.lineDerivOpCLM_eq, Bundle.Trivialization.symm_continuousLinearEquivAt_eq, ContinuousLinearMap.sum_comp_single, ContinuousLinearMap.instT2Space, Submodule.starProjection_apply_eq_isComplProjection, MeasureTheory.Lp.toTemperedDistributionCLM_apply, fderiv_iteratedFDeriv, ContinuousLinearMap.inner_map_map_of_mem_unitary, MeasureTheory.LpToLpRestrictCLM_coeFn, ContinuousLinearMap.hasFPowerSeriesOnBall, MDifferentiable.coordChangeL, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, ContinuousLinearMap.coe_add, MeasureTheory.setToFun_add_left, ContinuousLinearEquiv.conjContinuousAlgEquiv_refl, MeasureTheory.L1.SimpleFunc.norm_Integral_le_one, LinearMap.mkContinuous₂_norm_le', ContinuousLinearMap.rightInverse_of_comp, ContinuousLinearMap.toSpanSingleton_zero, ContinuousLinearMap.derivWithin_of_bilinear, TopModuleCat.hom_zero, Bundle.ContMDiffRiemannianMetric.isVonNBounded, HasDerivWithinAt.clm_comp, ContinuousLinearEquiv.equivOfInverse'_apply, SchwartzMap.lineDerivOpCLM_eq, SchauderBasis.norm_proj_le_nnnormProjBound, topDualPairing_isContPerfPair, TrivSqZeroExt.fstCLM_apply, MeasureTheory.condExpInd_of_measurable, cfcₙL_integral, HasStrictFDerivAt.fun_mul', LinearMap.mkContinuous₂_apply, ContinuousLinearMap.le_of_opNorm_le_of_le, fderivWithin_ofNat, ContinuousLinearMap.isPositive_iff_eq_sum_rankOne, HasMFDerivAt.mul, Bundle.ContMDiffRiemannianMetric.contMDiff, continuousOn_stereoToFun, Submodule.coe_continuous_linearProjOfClosedCompl', InnerProductSpace.isPositive_rankOne_self, WithSeminorms.banach_steinhaus, ContinuousLinearMap.isBigO_comp, ContinuousLinearEquiv.unitsEquiv_apply, ProbabilityTheory.isGaussian_iff_gaussian_charFun, ContinuousLinearMap.mulLeftRight_isBoundedBilinear, IsCompactOperator.clm_comp, LinearMap.mkContinuousOfExistsBound_apply, HasFDerivWithinAt.continuousMultilinearMap_apply, RCLike.map_apply, MDifferentiableOn.clm_postcomp, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, OrthonormalBasis.orthogonalProjection_eq_sum, ContinuousLinearMap.analyticWithinAt_bilinear, Complex.restrictScalars_one_smulRight', MeasureTheory.aestronglyMeasurable_condExpInd, HasCompactSupport.convolution_integrand_bound_left, ContinuousLinearMap.compSL_apply, ContinuousLinearMap.continuous₂, fderivWithin_comp_derivWithin_of_eq, ContinuousLinearMap.opNorm_prod, IsSelfAdjoint.quasispectrumRestricts, ContinuousLinearMap.integral_compLp, DoubleCentralizer.star_snd, ContinuousLinearMap.norm_inr_le_one, MeasureTheory.Measure.addHaar_image_continuousLinearMap, binomialSeries_eq_ordinaryHypergeometricSeries, Continuous.clm_comp_const, RCLike.ofRealCLM_apply, SchwartzMap.integral_sesq_fourier_fourier, HasMFDerivAt.add, Real.hasFDerivAt_fourierChar_neg_bilinear_left, ContinuousLinearMap.coe_comp', MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.convolution_eq_right', hasStrictFDerivAt_exp_of_mem_ball, ContinuousLinearMap.opNorm_le_of_unit_norm, curveIntegral_smul, MeasureTheory.L1.setToL1_indicatorConstLp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, extDeriv_constOfIsEmpty, ContinuousLinearMap.exists_preimage_norm_le, Convex.norm_image_sub_le_of_norm_fderivWithin_le', SchauderBasis.RankOneDecomposition.proj_tendsto, ContinuousAffineMap.neg_contLinear, Real.fderiv_fourierIntegral, hasStrictFDerivAt_list_prod_finRange', MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, LinearIsometry.nnnorm_toContinuousLinearMap, ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection, InnerProductSpace.rankOne_one_left_eq_innerSL, ContDiff.fderiv_succ, Submodule.IsOrtho.starProjection_comp_starProjection, fderiv_intCast, MDifferentiableAt.clm_bundle_apply, Filter.EventuallyEq.fderivWithin, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, fderivWithin_one, ContinuousLinearMap.continuous_det, ContinuousLinearMap.smulRight_one_eq_toSpanSingleton, PiTensorProduct.mapLMonoidHom_apply, MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv, ContinuousLinearMap.map_add_add, HasFDerivWithinAt.pow, ContinuousLinearMap.sSup_unit_ball_eq_norm, ContinuousAlternatingMap.norm_ofSubsingleton_id_le, hasFDerivWithinAt_const, hasFDerivAt_one, fderivWithin_fun_smul, ContinuousLinearMap.analyticWithinAt, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, complexOfReal_hasDerivWithinAt, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, HasFDerivWithinAt.add, TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, fderivWithin_fderivWithin_eq_of_mem_nhdsWithin, ContinuousLinearMap.toLinearMap₁₂_injective, curveIntegrable_segment, hasFDerivAt_multiset_prod, MDifferentiableAt.cle_arrowCongr, ContinuousLinearMap.frontier_preimage, ProbabilityTheory.covarianceBilinDual_apply', ContinuousAffineMap.fst_decompLinearEquiv, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, ContinuousLinearMap.smul_apply, ContinuousLinearMap.continuousSMul, hasFTaylorSeriesUpToOn_top_iff_right, ContinuousLinearMap.IsPositive.inner_left_eq_inner_right, conformalAt_iff, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, norm_jacobiTheta₂_term_fderiv_ge, AnalyticAtWithin.compContinuousLinearMap, ContinuousLinearMap.norm_inl_le_one, MeasureTheory.norm_condExpL2_le, SchwartzMap.pairing_apply_apply, InnerProductSpace.isIdempotentElem_rankOne_self, ContinuousLinearMap.opNorm_le_bound', Matrix.cstar_nnnorm_def, MeasureTheory.weightedSMul_apply, ContinuousLinearMap.comp_condExp_comm, Differentiable.clm_comp, intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, ApproximatesLinearOn.lipschitz, ContinuousLinearMap.continuous_integral_comp_L1, ContinuousLinearMap.isBigOWith_sub, ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, ClosedSubmodule.mem_comap, ContinuousLinearMap.isUniformEmbedding_restrictScalars, norm_iteratedFDerivWithin_one, TopModuleCat.hom_zero_apply, ContDiffAt.clm_apply, ContinuousLinearMap.hasDerivAtFilter, fderivWithin_csinh, DoubleCentralizer.intCast_snd, MeasureTheory.L1.norm_setToL1_le, HasDerivAtFilter.comp_hasFDerivAtFilter, DoubleCentralizer.range_toProdMulOpposite, ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall, hasFDerivAt_integral_of_dominated_loc_of_lip_interval, Submodule.re_inner_starProjection_eq_normSq, RCLike.conjCLE_norm, WeakSpace.map_apply, HasDerivWithinAt.complexToReal_fderiv', VectorField.fderiv_apply_lieBracket, MeasureTheory.inner_condExpL2_left_eq_right, ContinuousLinearMap.opNorm_ext, ContinuousMap.toLp_denseRange, IsCovariantDerivativeOn.difference_apply, ContinuousLinearMap.toContinuousAddMonoidHom_add, AnalyticOnNhd.compContinuousLinearMap, ContinuousLinearMap.integral_apply, Module.Basis.constrL_basis, ContinuousLinearMap.precompUniformConvergenceCLM_apply, ProbabilityTheory.covarianceBilinDual_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, ContinuousLinearMap.comp_memLp, Real.fderiv_fourierChar_neg_bilinear_right_apply, ContMDiffCovariantDerivativeOn.affine_combination, SchauderBasis.tendsto_proj, Real.fourier_continuousLinearMap_apply, banach_steinhaus_iSup_nnnorm, fderivWithin_fun_pow', SchauderBasis.proj_zero, intervalIntegral.fderiv_integral_of_tendsto_ae, ContDiffAt.fderiv_right_succ, ContinuousLinearEquiv.snd_equivOfRightInverse, toWeakSpaceCLM_bijective, Submodule.starProjection_orthogonal', HasFDerivWithinAt.clm_apply, DoubleCentralizer.natCast_fst, ContinuousLinearMap.norm_compLp_le, HasFPowerSeriesOnBall.unshift, Continuous.convolution_integrand_fst, ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries, ContDiffMapSupportedIn.structureMapCLM_apply, iteratedFDerivWithin_succ_eq_comp_right, ContinuousAffineMap.const_contLinear, eventually_enorm_mfderivWithin_symm_extChartAt_lt, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, tangentMap_snd, iteratedDerivWithin_vcomp_two, SchwartzMap.lineDerivOp_fourier_eq, ContinuousWithinAt.continuousLinearMapCoprod, HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq, innerSL_apply_apply, ContinuousLinearMap.IsInvertible.surjective, fderiv_multiset_prod, ContinuousLinearEquiv.subsingleton_or_norm_symm_pos, ProbabilityTheory.covarianceBilin_multivariateGaussian, SchwartzMap.integral_bilin_fourierInv_eq, TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars, VectorField.fderiv_apply_lieBracket_of_isSymmSndFDerivAt, HasFTaylorSeriesUpTo.hasFDerivAt, HasFDerivAtFilter.fun_sum, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, norm_iteratedFDerivWithin_clm_apply, ContMDiffWithinAt.mfderivWithin_const, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, ContinuousLinearMap.innerSL_apply_comp_of_isSymmetric, HasFDerivAtFilter.sub, Unitization.splitMul_apply, ContMDiffOn.clm_postcomp, ContinuousLinearMap.toBilinForm_apply, Measurable.apply_continuousLinearMap, Summable.mapL, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, DoubleCentralizer.nnnorm_def', LinearMap.adjoint_eq_toCLM_adjoint, HasFDerivAt.fun_mul, fderivWithin_zero_of_not_accPt, ContinuousLinearMap.map_zero, dist_iteratedFDerivWithin_one, Submodule.orthogonalProjection_mem_subspace_eq_self, ContinuousLinearMap.nnnorm_def, ContinuousLinearMap.IsPositive.inner_nonneg_right, DoubleCentralizer.zero_snd, TemperedDistribution.fourierMultiplierCLM_smul, ContinuousLinearMap.norm_compContinuousMultilinearMap_le, ContinuousLinearMap.completeSpace_eqLocus, LinearMap.mkContinuous_apply, ContinuousLinearMap.id_apply, HasFDerivWithinAt.hasLineDerivWithinAt, ContinuousLinearMap.opNorm_comp_linearIsometryEquiv, ProbabilityTheory.uncenteredCovarianceBilin_apply, TemperedDistribution.lineDerivOp_fourier_eq, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, FormalMultilinearSeries.derivSeries_coeff_one, VonNeumannAlgebra.ext_iff, Complex.ofRealCLM_norm, Submodule.starProjection_add_starProjection_orthogonal, mdifferentiableOn_symm_coordChangeL, ContinuousLinearMap.opNorm_lsmul_apply_le, ContDiffMapSupportedIn.fderivLM_eq_of_scalars, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, ContinuousLinearMap.intrinsicStar_toSpanSingleton, fderiv_clm_comp, ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian, SchwartzMap.bilinLeftCLM_apply, ContinuousLinearMap.intCast_apply, HasDerivAt.comp_hasFDerivAt_of_eq, ContinuousLinearMap.fpowerSeriesBilinear_apply_zero, GeneralSchauderBasis.tendsto_proj, IsConformalMap.is_complex_or_conj_linear, fderiv_continuousAlternatingMap_apply_const, ContinuousLinearMap.nhds_zero_eq_of_basis, MeasureTheory.L1.SimpleFunc.setToL1SCLM_const, SmoothBumpCovering.exists_immersion_euclidean, ContinuousLinearMap.coprodEquiv_apply, ContinuousLinearMap.cpolynomialAt, Submodule.starProjection_singleton, HasDerivAt.clm_apply, mfderiv_comp_apply_of_eq, ContinuousLinearMap.comp_condExp_add_const_comm, ContDiffMapSupportedIn.seminorm_fderivLM_le, Bundle.RiemannianMetric.isVonNBounded, ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, ContDiffMapSupportedIn.seminorm_fderivLM_top, ContinuousLinearMap.measurable, ContDiffWithinAt.clm_apply, curveIntegralFun_smul, Module.Basis.exists_opNorm_le, ContinuousLinearMap.coe_smul', WithLp.sndL_apply, GeneralSchauderBasis.proj_apply, hasStrictFDerivAt_iff_isLittleOTVS, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, DifferentiableOn.clm_apply, ContMDiff.clm_apply, ContinuousLinearMap.coe_restrictScalarsₗ, ContinuousLinearMap.applySMulCommClass', ProbabilityTheory.integral_continuousLinearMap_gaussianReal, Differentiable.fderiv_norm_rpow, fderivWithin_fderivWithin, FDerivMeasurableAux.le_of_mem_A, lintegral_fderiv_lineMap_eq_edist, ContinuousLinearMap.isBigOWith_id, ContinuousLinearMap.integrable_of_bilin_of_bdd_left, curveIntegrable_fun_neg_iff, TestFunction.monoCLM_eq_zero, ContinuousLinearMap.comp_inl_add_comp_inr, CurveIntegrable.zero, fderiv_comp_deriv, VectorField.mlieBracket_smul_left, ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one, curveIntegrable_smul_iff, ContDiffOn.clm_apply, ContinuousLinearMap.opNNNorm_le_iff, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1, ContinuousLinearMap.isometry_mul_flip, BoundedContinuousFunction.evalCLM_apply, HasStrictFDerivAt.mul', inner_gradientWithin_right, fderiv_fun_pow, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective, HasStrictFDerivAt.comp_hasStrictDerivAt, ContinuousLinearMap.adjoint_id, Complex.hasStrictFDerivAt_exp_real, HasFDerivAtFilter.const_sub, LinearMap.coe_toContinuousLinearMap', HasFDerivWithinAt.linear_multilinear_comp, iteratedFDerivWithin_succ_eq_comp_left, ContinuousLinearMap.isPositive_natCast, hasStrictFDerivAt_exp_smul_const_of_mem_ball', ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, Submodule.starProjection_comp_starProjection_eq_zero_iff, FDerivMeasurableAux.differentiable_set_subset_D, SchwartzMap.laplacianCLM_eq, fderiv_fun_smul, CStarModule.innerSL_apply, ContinuousLinearMap.hasDerivWithinAt_of_bilinear, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, ContinuousAffineMap.fst_decompEquiv, LinearIsometryEquiv.conjStarAlgEquiv_apply, Bundle.ContinuousLinearMap.vectorBundle, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image, HasFDerivAt.le_of_lipschitzOn, contDiff_one_iff_fderiv, MeasureTheory.ConvolutionExistsAt.integrable, HasStrictFDerivAt.pow, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, ProbabilityTheory.covarianceOperator_apply, fderivWithin_sinh, algebraMapCLM_coe, ContDiffAt.laplacian_CLM_comp_left, HasStrictFDerivAt.const_mul, ContinuousLinearMap.coe_zero', Distribution.IsVanishingOn.smulLeftCLM, ContinuousLinearMap.smulRight_one_pow, ContinuousLinearMap.opNorm_mul_flip_apply, ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, ConvexOn.univ_sSup_of_countable_affine_eq, ContinuousLinearMap.ebound, Submodule.coe_subtypeL', InnerProductSpace.inner_left_rankOne_apply, integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable, norm_iteratedFDeriv_clm_apply, TestFunction.toBoundedContinuousFunctionCLM_apply, ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse, HasFDerivAt.finset_prod, ContinuousLinearMap.ofMemClosureImageCoeBounded_apply, SchwartzMap.fderivCLM_apply, ContinuousLinearMap.smul_compLp, Submodule.norm_starProjection_apply_le, TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, IsLocalMax.fderiv_eq_zero, ContinuousLinearMap.contMDiff, ContinuousLinearMap.mdifferentiable, HasStrictFDerivAt.fun_sum, HasFDerivAt.norm_sq, VectorBundleCore.coordChange_self, ContinuousAlternatingMap.curryLeft_smul, fderiv_const_smul_field, LinearIsometry.map_starProjection', ContinuousLinearMap.hasBasis_nhds_zero, Continuous.clm_comp, cfcL_apply, Real.hasStrictFDerivAt_rpow_of_pos, DoubleCentralizer.pow_snd, LinearIsometry.coe_toContinuousLinearMap, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt, ContDiffAt.continuousAt_fderiv, fderiv_fun_pow', Real.integrable_prod_sub, ContinuousLinearMap.eq_adjoint_iff, ContinuousLinearMap.hasFDerivAt, fderivWithin_intCast, Submodule.starProjection_tendsto_self, ContDiffAt.fderiv_succ, ContinuousLinearMap.topologicalAddGroup, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star, SchwartzMap.toLpCLM_apply, ContinuousLinearMap.single_apply, ContinuousLinearMap.toSpanSingleton_apply, LinearMap.IsSymmetric.directSum_decompose_apply, ContinuousLinearMap.sum_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, HasFDerivAt.continuousMultilinear_apply_const, HasFDerivWithinAt.continuousAlternatingMap_apply, ContinuousLinearMap.IsPositive.smul_of_nonneg, InnerProductSpace.rankOne_apply, Unitary.coe_linearIsometryEquiv_apply, HasFDerivAt.of_notMem_tsupport, fderiv_sum, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, HarmonicAt.analyticAt_complex_partial, MeasureTheory.SimpleFunc.setToSimpleFunc_const, ContinuousLinearMap.toSpanSingleton_apply_one, HasStrictDerivAt.clm_comp, HasFDerivWithinAt.const_mul, ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator, MeasureTheory.weightedSMul_nonneg, cfcₙ_eq_cfcₙL_mkD, fderiv_ofNat, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMap.toLp_norm_le, ContinuousMultilinearMap.norm_smulRightL_le, derivWithin_clm_comp, ContinuousLinearMap.precompL_apply, DoubleCentralizer.nnnorm_snd, IsSelfAdjoint.adjoint_eq, Bundle.Pretrivialization.continuousLinearMap_apply, Submodule.reflection_apply, curveIntegralFun_segment, HasDerivWithinAt.clm_apply, ContinuousLinearMap.coe_mkOfIsCompactOperator, fderivWithin_zero, RKHS.kernel_apply, curveIntegral_neg, LinearMap.IsContPerfPair.bijective_left, HasFDerivAt.sub, VectorBundleCore.contMDiffOn_coordChange, MDifferentiable.clm_postcomp, InnerProductSpace.gramSchmidt_def, ContinuousLinearMap.completeSpace, CStarMatrix.toCLM_injective, enorm_fderiv_norm_rpow_le, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, ContinuousLinearMap.isPositive_self_comp_adjoint, ContinuousLinearMap.hasFPowerSeriesAt, LinearMap.adjoint_toContinuousLinearMap, fderivWithin_const_sub, Unitary.linearIsometryEquiv_coe_apply, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivAtFilter.neg, fderiv_eq_deriv_mul, Submodule.starProjection_inner_eq_zero, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, ContinuousLinearMap.toSesqForm_apply_coe, coe_algebraMapCLM, HasFDerivWithinAt.fun_const_smul, HasStrictFDerivAt.const_smul, hasStrictFDerivAt_natCast, HasFPowerSeriesWithinOnBall.fderivWithin, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, FormalMultilinearSeries.radius_compNeg, hasFDerivAtFilter_ofNat, hasFDerivAtFilter_zero, HasFDerivAt.multilinear_comp, BoxIntegral.hasIntegral_GP_pderiv, ContinuousMultilinearMap.linearDeriv_apply, SchwartzMap.integral_bilin_fourierIntegral_eq, ContinuousAffineMap.decomp, LinearIsometryEquiv.adjoint_eq_symm, fderivWithin_ccosh, ContinuousAlternatingMap.toAlternatingMap_curryLeft, ContinuousLinearMap.toLinearMap₁₂_apply, HasFDerivWithinAt.mul, Submodule.IsOrtho.orthogonalProjection_comp_subtypeL, ContinuousLinearMap.sSup_sphere_eq_nnnorm, VectorFourier.fourierPowSMulRight_eq_comp, ContinuousLinearMap.finiteDimensional, ContinuousLinearMap.hasFDerivWithinAt_of_bilinear, fderivWithin_const_mul, HasFDerivWithinAt.multiset_prod, ContinuousLinearMap.opNorm_mul, DoubleCentralizer.smul_toProd, mfderivWithin_projIcc_one, ContDiffMapSupportedIn.fderivCLM_apply_of_gt, TestFunction.fderivCLM_apply_of_le, TemperedDistribution.smulLeftCLM_neg, HasFDerivAt.arctan, PiTensorProduct.mapL_one, ContinuousLinearMap.smulRight_zero, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, DoubleCentralizer.toProdMulOpposite_injective, ContinuousLinearMap.norm_fst_le, MDifferentiable.cle_arrowCongr, PointwiseConvergenceCLM.postcomp_apply, ContMDiffAt.mfderiv_apply, MeasureTheory.dominatedFinMeasAdditive_condExpInd, Complex.reCLM_nnnorm, ContinuousLinearMap.map_sub, DoubleCentralizer.norm_fst_eq_snd, Unitization.nnnorm_def, ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, ContinuousLinearMap.le_opNorm, TestFunction.fderivCLM_ofSupportedIn, HasFDerivAt.fun_smul, fderivWithin_fun_neg, ContinuousLinearMap.flipMultilinear_apply_apply, fderiv_continuousAlternatingMapCompContinuousLinearMap, compactOperator_topologicalClosure, ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply, ContinuousLinearMap.isEmbedding_postcomp, PiTensorProduct.mapL_smul, SchwartzMap.integral_sesq_fourier_eq, MeasureTheory.aestronglyMeasurable_condExpL2, cfcL_integrable, MeasureTheory.L1.SimpleFunc.setToL1S_add_left, Submodule.orthogonalProjection_bot, Real.fderiv_fourier, DoubleCentralizer.norm_def', ApproximatesLinearOn.norm_fderiv_sub_le, ContinuousLinearMap.adjointAux_norm, MeasureTheory.L1.setToL1_smul_left, ContinuousWithinAt.clm_apply_of_inCoordinates, CStarMatrix.norm_def', MDifferentiable.clm_bundle_apply₂, ContinuousLinearMap.fderiv, ContinuousLinearMap.smul_comp, fderiv_neg, MeasureTheory.L1.setToL1_zero_left, ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousLinearMap.comp_add, EuclideanGeometry.orthogonalProjection_apply_mem, ContinuousLinearMap.integrableAtFilter_comp, ContinuousAffineMap.smul_contLinear, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, ProbabilityTheory.covarianceBilin_apply_basisFun_self, HasDerivAt.comp_hasFDerivWithinAt, MeasureTheory.condExpInd_nonneg, ContinuousLinearMap.hasStrictFDerivAt_of_bilinear, ContinuousLinearMap.fpowerSeries_apply_zero, VectorPrebundle.mk_contMDiffCoordChange, ContinuousLinearMap.mul_apply, extDerivWithin_constOfIsEmpty, VectorFourier.fourierIntegral_continuousLinearMap_apply, ContinuousAffineMap.norm_def, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, ContinuousLinearMap.IsInvertible.bijective, ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left, ContinuousLinearEquiv.coeFn_ofBijective, ContinuousLinearMap.integral_comp_comm', Pi.compRightL_apply, ContinuousLinearMap.comp_memLp', HasStrictFDerivAt.list_prod', ContinuousLinearMap.map_smul_of_tower, SchwartzMap.fourier_lineDerivOp_eq, LinearMap.toContinuousBilinearMap_apply, norm_iteratedFDerivWithin_clm_apply_const, ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith, CStarMatrix.inner_toCLM_conjTranspose_left, isBoundedBilinearMap_comp, fderivWithin_sin, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, ContinuousAlgHom.coe_toContinuousLinearMap, ContinuousLinearMap.pi_apply, TemperedDistribution.fourierInv_lineDerivOp_eq, MeasureTheory.condExpL2_indicator_ae_eq_smul, ContinuousLinearMap.exists_lt_apply_of_lt_opNorm, fderiv_fun_sub, mfderivWithin_comp_projIcc_one, IsMIntegralCurveOn.hasDerivWithinAt, Bundle.Trivialization.coe_continuousLinearEquivAt_eq, ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply, DoubleCentralizer.norm_def, Complex.hasStrictFDerivAt_cpow', HasCompactSupport.fderiv, Real.fourier_iteratedFDeriv, SchwartzMap.smulLeftCLM_real_smul, HasMFDerivAt.smul, hasFDerivWithinAt_intCast, contDiff_succ_iff_fderiv, PositiveLinearMap.leftMulMapPreGNS_apply, ContinuousLinearMap.opNNNorm_prod, MeasureTheory.condExpL1CLM_of_aestronglyMeasurable', ContinuousAffineMap.decompEquiv_symm_contLinear, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable, MDifferentiableAt.clm_prodMap, ContinuousLinearMap.intrinsicStarModule, InnerProductSpace.HarmonicOnNhd.comp_CLM, HasMFDerivAt.neg, ContinuousLinearMap.one_smulRight_eq_toSpanSingleton, HasFDerivAt.fun_const_smul, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, UnitAddTorus.mFourierCoeff_toLp, ProbabilityTheory.gaussianReal_map_continuousLinearMap, Manifold.pathELength_def, ContinuousLinearMap.uniformContinuous_restrictScalars, ContinuousLinearMap.mulLeftRight_apply, curveIntegral_fun_smul, fromTangentSpace_mfderiv_smul_apply, ProbabilityTheory.covarianceOperator_zero, Bundle.ContinuousRiemannianMetric.symm, ContinuousMultilinearMap.curryRight_norm, ContinuousLinearMap.analyticOn_bilinear, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left', InnerProductSpace.unique_continuousLinearMapOfBilin, fderiv.log, FDerivMeasurableAux.norm_sub_le_of_mem_A, HasFDerivAt.add, ContinuousLinearMap.deriv, hasStrictFDerivAt_multiset_prod, ContinuousLinearMap.continuous_of_continuous_uncurry, MDifferentiableAt.clm_postcomp, fderiv_continuousAlternatingMap_apply, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, curveIntegral_fun_zero, MDifferentiable.clm_bundle_apply, coe_innerSL_apply, ContinuousAlternatingMap.ofSubsingleton_apply_toContinuousMultilinearMap, fderivWithin_finset_prod, HasFDerivWithinAt.const_sub, ContinuousLinearMap.isCompact_image_coe_closedBall, RegularNormedAlgebra.isometry_mul', ContDiffWithinAt.hasFDerivWithinAt_nhds, HasFDerivAt.sum, ContinuousLinearMap.isClosed_image_coe_closedBall, DoubleCentralizer.central, ContinuousLinearMap.coe_neg', MeasureTheory.integral_condExpL2_eq, IsCovariantDerivativeOn.torsion_self, ContinuousLinearMap.instStarOrderedRing, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, hasFDerivAtFilter_const, VectorBundleCore.localTriv_symm_fst, MDifferentiableWithinAt.clm_bundle_apply₂, TestFunction.limitCLM_apply, ContinuousAffineMap.decompLinearEquiv_symm_contLinear, hasFDerivAtFilter_iff_isLittleO, ContinuousLinearEquiv.one_le_norm_mul_norm_symm, HasFDerivAt.clm_apply, eventually_norm_mfderivWithin_symm_extChartAt_lt, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, ContinuousLinearMap.hasDerivAt, ContinuousLinearMap.antilipschitz_of_isEmbedding, VectorFourier.hasFDerivAt_fourierIntegral, hasFDerivAt_ringInverse, contDiffAt_one_iff, HasFDerivAt.continuousAlternatingMap_apply, MeasureTheory.convolution_precompR_apply, HasFDerivWithinAt.of_notMem_tsupport, ContinuousLinearMap.instCStarRingId, SchwartzMap.compSubConstCLM_apply, Matrix.linfty_opNNNorm_eq_opNNNorm, VectorFourier.fourierIntegral_iteratedFDeriv, HasMFDerivWithinAt.neg, ContinuousCohomology.I_obj_ρ_apply, UnconditionalSchauderBasis.enorm_proj_le_enormProjBound, MeasureTheory.setIntegral_condExpL2_indicator, InnerProductSpace.nnnorm_rankOne, fderiv_smul, LinearIsometry.norm_toContinuousLinearMap, OrthonormalBasis.orthogonalProjection_apply_eq_sum, ContinuousLinearEquiv.arrowCongr_apply, MeasureTheory.SimpleFunc.setToSimpleFunc_add_left, ContinuousLinearMap.range_toLinearMap, ContinuousLinearMap.norm_toSpanSingleton, fderivWithin_eventually_congr_set', ContinuousLinearMap.coe_equivRange, ContinuousLinearMap.setIntegral_compLp, VectorField.fderivWithin_pullbackWithin, ContinuousLinearMap.toUniformConvergenceCLM_apply, ContinuousLinearMap.interior_preimage, ContinuousAlternatingMap.curryLeft_apply_apply, ContinuousLinearMap.flip_smul, ContinuousLinearMap.contDiffPointwiseHolderAt, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, SeparationQuotient.outCLM_uniformContinuous, InnerProductSpace.isSymmetricProjection_rankOne_self, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, RKHS.isHermitian_kernel, Module.Basis.constrL_apply, MeasureTheory.L1.setToL1_mono_left', ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, hasMFDerivAt_neg, HasFDerivWithinAt.const_smul, MeasureTheory.ConvolutionExistsAt.integrable_swap, ContinuousOn.clm_comp, SchwartzMap.laplacianCLM_eq', VectorBundleCore.trivializationAt_coordChange_eq, DoubleCentralizer.nnnorm_def, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, ContinuousLinearMap.measurable_apply₂, DifferentiableAt.fderiv_norm_self, continuousOn_tangentCoordChange, ContMDiffCovariantDerivativeOn.finite_affine_combination, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, ContDiff.continuous_fderiv_apply, fderivWithin_continuousAlternatingMap_apply_const_apply, ContinuousLinearMap.norm_eq_iSup_rayleighQuotient, ContinuousLinearMap.const_apply_apply, ContinuousAt.clm_apply, SeparatingDual.dualMap_surjective_iff, IsLocalExtr.fderiv_eq_zero, EuclideanGeometry.orthogonalProjection_apply', HasFPowerSeriesOnBall.fderiv_eq, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, ContinuousLinearMap.opNorm_le_of_shell', ContinuousLinearMap.restrictScalars_neg, ContinuousLinearMap.instLocallyConvexSpace, IsCovariantDerivativeOn.smul_const, NormedSpace.inclusionInDoubleDual_norm_eq, ContinuousLinearMap.uniformContinuous, SchwartzMap.smulLeftCLM_sum, ContinuousLinearEquiv.conjContinuousAlgEquiv_trans, ContinuousLinearMap.proj_apply, mfderiv_prod_eq_add_comp, ContinuousAffineMap.decompLinearIsometryEquiv_symm_apply, ContinuousLinearMap.fderiv_of_bilinear, has_fderiv_at_filter_real_equiv, hasFDerivAt_of_subsingleton, unitary.linearIsometryEquiv_coe_symm_apply, ContinuousLinearMap.coe_mul', MeasureTheory.setIntegral_condExpInd, ContinuousLinearMap.nnnorm_toSpanSingleton, iteratedFDerivWithin_succ_apply_right, ContinuousAlternatingMap.alternatizeUncurryFin_smul, contDiffAt_map_inverse, fderiv_mul_const', RKHS.posSemidef_tfae, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, SchwartzMap.toBoundedContinuousFunctionCLM_apply, extDeriv_apply_vectorField, ContDiffMapSupportedIn.monoCLM_eq_of_scalars, curveIntegral_segment, TestFunction.postcompCLM_apply, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, CovariantDerivative.torsion_apply, Real.fourierIntegral_continuousLinearMap_apply, Submodule.starProjection_top', Submodule.adjoint_subtypeL, IsCovariantDerivativeOn.torsion_antisymm, hasStrictFDerivAt_exp, AnalyticOn.fderivWithin, ContinuousLinearMap.opNorm_mul_apply, ContinuousLinearMap.norm_smulRightL, ContinuousLinearMap.intrinsicStar_comp, NormedSpace.inclusionInDoubleDualWeak_apply_apply, HasFDerivWithinAt.fun_smul, ContinuousLinearMap.isBigO_id, MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable, ContDiffAt.fderiv_right, AnalyticOn.compContinuousLinearMap, hasStrictFDerivAt_iff_isLittleO, MeasureTheory.convolution_def, MeasureTheory.norm_condExpL2_coe_le, ContMDiffFiberwiseLinear.locality_aux₂, ContinuousMultilinearMap.curryLeft_norm, HasStrictFDerivAt.of_notMem_tsupport, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, ContinuousLinearMap.compContinuousMultilinearMapL_apply, InnerProductSpace.trace_rankOne, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, MDifferentiableWithinAt.cle_arrowCongr, ContinuousLinearMap.exists_approx_preimage_norm_le, MeasureTheory.L1.setToL1_nonneg, FDerivMeasurableAux.D_subset_differentiable_set, LinearMap.IsSymmetric.isSelfAdjoint, MDifferentiableWithinAt.clm_precomp, SchwartzMap.fourierMultiplierCLM_sum, FDerivMeasurableAux.differentiable_set_eq_D, ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed, ContMDiffVectorBundle.continuousLinearMap, ContinuousLinearMap.summable, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, ContDiffOn.fderiv_of_isOpen, ContinuousLinearMap.continuous_restrictScalars, HasFDerivWithinAt.neg, isBoundedBilinearMap_compMultilinear, Submodule.isIdempotentElem_starProjection, hasFDerivAt_norm_rpow, ContinuousLinearMap.toLinearMapRingHom_apply, ContinuousLinearMap.compL_apply, ContinuousLinearMap.lsmul_flip_inj, MeasureTheory.Measure.addHaar_preimage_continuousLinearMap, DoubleCentralizer.neg_snd, summable_jacobiTheta₂_term_fderiv_iff, ContinuousLinearMap.ringInverse_equiv, ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM, ContinuousLinearMap.analyticAt, ContinuousLinearMap.isInvertible_zero_iff, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, HasFPowerSeriesWithinAt.fderivWithin_eq, RKHS.kerFun_apply, Matrix.linfty_opNNNorm_toMatrix, inCoordinates_apply_eq₂, AnalyticOnNhd.fderiv_of_isOpen, FourierTransform.fourierInvCLM_apply, MeasureTheory.L1.integral_def, contDiffOn_infty_iff_fderivWithin, ContinuousLinearMap.IsPositive.conj_adjoint, ContinuousLinearMap.flip_apply, hasFDerivAt_iff_isLittleO, tangentMapWithin_snd, Matrix.toEuclideanCLM_toLp, ContinuousLinearMap.pi_eq_zero, ContinuousCohomology.Iobj_ρ_apply, ContinuousAt.clm_apply_of_inCoordinates, ProbabilityTheory.covarianceBilin_zero, HasFDerivAt.comp_hasDerivAt, contDiffOn_stereoToFun, Real.hasFDerivAt_fourier, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, ContinuousLinearMap.isUniformAddGroup, Unitary.coe_symm_linearIsometryEquiv_apply, fderiv_inverse, hasStrictFDerivAt_exp_smul_const', SchwartzMap.smulLeftCLM_fun_neg, HasFPowerSeriesOnBall.fderiv, ContMDiffOn.clm_precomp, BoundedContinuousFunction.toLp_inj, ContinuousMultilinearMap.restrictScalarsLinear_apply, ImplicitFunctionData.leftDeriv_fderiv_implicitFunction, measurableSet_of_differentiableAt_of_isComplete, ContinuousLinearMap.toSpanSingleton_apply_map_one, HilbertBasis.hasSum_orthogonalProjection, ContinuousLinearMap.bilinearRestrictScalars_apply_apply, ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map, Complex.hasStrictFDerivAt_cpow, InnerProductSpace.adjoint_rankOne, ContinuousLinearMap.compFormalMultilinearSeries_apply', fderiv_pow, InnerProductSpace.rankOne_eq_zero, ContinuousLinearMap.lipschitz, DoubleCentralizer.range_toProd, Real.fourierIntegral_convergent_iff', fderiv_one, fderivWithin_continuousMultilinear_apply_const_apply, ContinuousAffineMap.coe_linear_eq_coe_contLinear, BoundedContinuousFunction.toLp_injective, Unitization.splitMul_injective_of_clm_mul_injective, ContinuousAlternatingMap.norm_curryLeft, Submodule.norm_sq_eq_add_norm_sq_starProjection, Bundle.ContMDiffRiemannianMetric.symm, ContMDiffOn.coordChangeL, InnerProductSpace.inner_right_rankOne_apply, VectorField.fderiv_pullback, SchwartzMap.pairing_apply, HasFDerivAt.pow, ContinuousLinearMap.exists_right_inverse_of_surjective, mfderivWithin_extChartAt_symm_inverse_apply, fderivWithin_comp_derivWithin, ContDiff.continuous_fderiv, ContinuousAlternatingMap.apply_apply, mdifferentiableAt_hom_bundle, HasFPowerSeriesWithinOnBall.unshift, innerSL_inj, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_inv', MeasureTheory.lintegral_nnnorm_condExpL2_le, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, StrongDual.toLp_of_not_memLp, ContinuousLinearMap.eqOn_closure_span, ContinuousLinearMap.fderivWithin_of_bilinear, HasFPowerSeriesOnBall.compContinuousLinearMap, DoubleCentralizer.add_fst, MeasureTheory.L1.setToFun_eq_setToL1, LinearMap.IsSymmetric.coe_toSelfAdjoint, ContinuousWithinAt.clm_comp, ContinuousLinearMap.applyFaithfulSMul, GeneralSchauderBasis.proj_apply_basis_mem, SeparationQuotient.outCLM_isUniformEmbedding, PiTensorProduct.liftIsometry_tprodL, HasStrictFDerivAt.cexp, NormedSpace.inclusionInDoubleDual_norm_le, ContinuousMultilinearMap.ofSubsingleton_symm_apply_apply, SeparatingDual.instNontrivialContinuousLinearMapIdOfContinuousSMul, curveIntegral_segment_const, mfderiv_sub, VectorBundleCore.localTriv_symm_apply, MeasureTheory.L1.integral_eq_setToL1, Convex.second_derivative_within_at_symmetric, BoxIntegral.BoxAdditiveMap.volume_apply, TangentBundle.trivializationAt_apply, ConvexOn.sSup_of_countable_affine_eq, TestFunction.coe_ofSupportedInCLM, LinearMap.norm_mkContinuous₂_aux, InnerProductSpace.rankOne_eq_rankOne_iff_comm, ContinuousLinearMap.uniformContinuousConstSMul, ContinuousLinearMap.toContinuousAddMonoidHom_zero, ContinuousLinearMap.leftInverse_of_comp, ContinuousLinearMap.norm_map_of_mem_unitary, ContinuousLinearMap.derivWithin, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, ContinuousLinearMap.precompR_apply, ContinuousAffineMap.norm_eq, HarmonicAt.differentiableAt_complex_partial, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, HasFDerivWithinAt.mul_const, hasFDerivWithinAt_iff_isLittleO, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd', ContinuousLinearMap.homeomorphOfUnit_apply, MeasureTheory.hasFDerivAt_convolution_right_with_param, ProbabilityTheory.IsGaussian.charFun_eq', fderiv_pow', ProbabilityTheory.covarianceBilinDual_eq_covariance, ContMDiffAt.mfderiv_const, fderiv_mul, MeasureTheory.condExpL1CLM_indicatorConstLp, SchwartzMap.postcompCLM_apply, ContinuousLinearMap.ratio_le_opNorm, ContinuousLinearMap.toSpanSingleton_pow, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, HasStrictFDerivAt.isLittleO, HasCompactSupport.hasFDerivAt_convolution_right, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, ContDiffMapSupportedIn.structureMapCLM_zero_apply, VonNeumannAlgebra.centralizer_centralizer', TrivSqZeroExt.sndCLM_apply, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ContinuousAlternatingMap.curryLeft_compContinuousAlternatingMap, ProbabilityTheory.covarianceBilinDual_zero, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, MeasureTheory.L1.setToL1_add_left', Submodule.norm_orthogonalProjection_apply_le, Continuous.fderiv, ContinuousLinearMap.coe_pow', InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, DoubleCentralizer.smul_fst, ContMDiffAt.clm_apply_of_inCoordinates, ContinuousLinearMap.coprod_add, norm_fderiv_le_of_lipschitz, Bundle.Pretrivialization.continuousLinearMap.isLinear, MeasureTheory.L1.setToL1_mono_left, TangentBundle.coordChange_model_space, ContinuousLinearMap.adjoint_inner_left, MeasureTheory.condExpInd_disjoint_union, fderivWithin_cos, ContinuousLinearMap.hasStrictDerivAt_of_bilinear, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, Continuous.clm_bundle_apply, ContinuousLinearEquiv.arrowCongr_symm, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, compContinuousLinearMap_zero, ContinuousMultilinearMap.ofSubsingletonₗᵢ_symm_apply, fderivWithin_continuousMultilinear_apply_const, TopModuleCat.hom_add, Differentiable.fderiv_two, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le, MeasureTheory.weightedSMul_empty, ContinuousLinearMap.toSpanSingleton_smul, ContinuousLinearMap.instContinuousEvalConst, fderivWithin_ccos, ContinuousAffineMap.fst_decompAffineEquiv, MDifferentiableOn.coordChangeL, VectorField.lieBracketWithin_smul_left, ContinuousAlternatingMap.ofSubsingletonLIE_apply, fderiv_fun_add, continuousMultilinearCurryRightEquiv_symm_apply, TemperedDistribution.fourierMultiplierCLM_apply, SchwartzMap.lineDeriv_eq_fourierMultiplierCLM, ContinuousLinearMap.hasSum, ContinuousLinearMap.coe_smulRightₗ, ContinuousLinearMap.lipschitz_apply, IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real, fderiv_pow_ring, ContinuousLinearMap.lsmul_apply, extDerivWithin_apply_vectorField_of_pairwise_commute, ContinuousLinearMap.rayleighQuotient_zero_apply, LinearIsometryEquiv.conjStarAlgEquiv_trans, Bundle.ContMDiffRiemannianMetric.pos, HasDerivWithinAt.complexToReal_fderiv, ContinuousLinearMap.equivRange_symm_apply, ContinuousLinearMap.bilinearComp_zero_right, ContinuousLinearMap.opNNNorm_le_bound, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, ContinuousLinearMap.toContinuousAddMonoidHom_comp, IsContMDiffRiemannianBundle.exists_contMDiff, ContinuousLinearMap.comp_finset_sum, ContDiffWithinAt.fderivWithin'', Complex.ofRealCLM_nnnorm, Complex.imCLM_norm, ContinuousLinearMap.iteratedFDerivWithin_comp_left, InnerProductSpace.rank_rankOne, ContMDiffOn.cle_arrowCongr, ContinuousLinearMap.HasRightInverse.rightInverse_rightInverse, ContMDiffAt.clm_bundle_apply, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner, Convex.taylor_approx_two_segment, MDifferentiableOn.clm_prodMap, contMDiffAt_coordChangeL, HasFDerivWithinAt.fun_sub, ContinuousLinearMap.adjointAux_apply, ContinuousLinearMap.nonneg_iff_isPositive, fderivWithin_fun_sub, ContinuousAffineMap.norm_contLinear_le, ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self, IsCompactOperator.hasEigenvalue_or_mem_resolventSet, fderivWithin_fun_mul', ProbabilityTheory.IsGaussianProcess.comp_left, ContinuousMap.evalCLM_apply, ProperCone.innerDual_singleton, VonNeumannAlgebra.coe_mk, ContinuousLinearMap.isUniformInducing_postcomp, TemperedDistribution.fourierMultiplierCLM_const, ContDiffWithinAt.continuousLinearMap_comp, Continuous.clm_apply, ContinuousAlternatingMap.norm_ofSubsingleton, hasFDerivAt_list_prod', hasFDerivAt_integral_of_dominated_loc_of_lip', RKHS.kerFun_dense, InnerProductSpace.rankOne_def, MDifferentiableWithinAt.coordChangeL, ContinuousLinearMap.smulCommClass, ContinuousLinearMap.coe_flipₗᵢ', MDifferentiableAt.clm_bundle_apply₂, MeasureTheory.weightedSMul_null, stereoToFun_apply, ContinuousLinearMap.adjointAux_inner_left, ContinuousLinearMap.coe_coe, SchwartzMap.convolution_apply, Submodule.sub_starProjection_mem_orthogonal, contDiffOn_succ_iff_fderiv_of_isOpen, hasSum_jacobiTheta₂_term_fderiv, Polynomial.fderiv_aeval, fderivWithin_fderivWithin_eq_of_mem_nhds, ContinuousLinearMap.norm_smulRight_apply, ConvexOn.real_univ_sSup_of_countable_affine_eq, ContinuousLinearMap.add_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, HasSum.mapL, fderiv_mul', UniformSpace.Completion.norm_toComplL, ContinuousLinearMap.coe_projKerOfRightInverse_apply, fderivWithin_const_smul_of_field, ProbabilityTheory.covarianceBilin_comm, ContinuousMap.toLp_def, ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker, VectorField.lieBracket_fmul_left, HasFDerivAtFilter.sum, SchwartzMap.integral_bilin_fourier_eq, HasFDerivWithinAt.lim, DifferentiableOn.clm_comp, ContDiffMapSupportedIn.monoCLM_apply, ClosedSubmodule.orthogonal_eq_inter, ContinuousLinearMap.toLinearMap_intrinsicStar, HasFDerivWithinAt.cexp, hasFDerivWithinAt_iff_hasDerivWithinAt, ProperCone.coe_comap, hasFTaylorSeriesUpToOn_succ_iff_right, ContinuousOn.clm_bundle_apply₂, ContinuousLinearMap.coe_flipMultilinearEquiv, NonUnitalAlgHom.coe_Lmul, ContinuousMultilinearMap.norm_map_init_le, ContinuousLinearMap.iteratedFDerivWithin_comp_right, ContinuousLinearMap.isIdempotentElem_toLinearMap_iff, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain, SchwartzMap.compCLMOfAntilipschitz_apply, SchwartzMap.fourierInv_apply_eq, SchwartzMap.smulRightCLM_apply_apply, LinearIsometryEquiv.conjStarAlgEquiv_refl, CurveIntegrable.fun_zero, MeasureTheory.setToFun_smul_left, HasDerivAt.complexToReal_fderiv', hasStrictFDerivAt_iff_hasStrictDerivAt, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin, MeasureTheory.L1.setToL1_smul_left', VectorField.mpullback_apply, LinearMap.IsSymmetric.toSelfAdjoint_apply, ContDiffWithinAt.continuousWithinAt_fderivWithin, fderiv_mem_iff, MeasureTheory.aemeasurable_fderivWithin, TopModuleCat.hom_zsmul, ContinuousLinearMap.zero_comp, VectorField.lieBracket_eq, fderiv_norm_smul_neg, SchwartzMap.toTemperedDistributionCLM_apply_apply, ContinuousLinearMap.coe_restrict_scalarsL', HasDerivAt.complexToReal_fderiv, fderivWithin_fderivWithin_eq_of_eventuallyEq, DoubleCentralizer.star_fst, PiTensorProduct.liftEquiv_symm_apply, TestFunction.coe_ofSupportedInLM, mfderivWithin_eventually_congr_set', Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable, ContMDiffOn.clm_comp, SchauderBasis.proj_apply, CovariantDerivative.affine_combination_toFun, hasFDerivAt_exp_smul_const', Bundle.Trivialization.continuousLinearMapAt_symmL, iteratedFDerivWithin_one_apply, ContinuousLinearMap.restrictScalars_add, TemperedDistribution.smulLeftCLM_sub, fromTangentSpace_mfderiv_smul', HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall, IsCoercive.bounded_below, SchwartzMap.postcompCLM_postcompCLM, Submodule.norm_subtypeL, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear, ContinuousLinearMap.map_tsum, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, ContinuousLinearMap.aestronglyMeasurable_comp₂, SchwartzMap.smulLeftCLM_const, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left, MeasureTheory.setToFun_indicator_const, ContinuousMapZero.toContinuousMapCLM_apply, ContinuousAffineMap.sub_contLinear, HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt, ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff, ContinuousLinearMap.IsIdempotentElem.TFAE, ContinuousLinearMap.opNorm_le_of_ball, fderiv_fun_sum, ContinuousAffineMap.decompLinearIsometryEquiv_symm_contLinear, Complex.hasFDerivAt_cpow, LinearEquiv.extendOfIsometry_symm_apply, Submodule.norm_sq_eq_add_norm_sq_projection, tangentCoordChange_comp, HasFDerivWithinAt.fun_neg, MeasureTheory.setToFun_zero_left, LinearMap.range_toContinuousLinearMap, fderiv_const_smul_of_invertible, Matrix.inner_toEuclideanCLM, ContinuousLinearMap.norm_precompR_le, hasFDerivWithinAt_pow', HasFTaylorSeriesUpToOn.continuousLinearMap_comp, SchauderBasis.bddAbove_range_nnnorm_proj, ContinuousLinearMap.hasFDerivAtFilter, ContinuousLinearMap.isBoundedLinearMap_comp_right, HasFDerivAt.iterate, Submodule.starProjection_apply, ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear, ContinuousLinearMap.eventually_nhds_zero_mapsTo, LineDeriv.laplacianCLM_eq_sum, VonNeumannAlgebra.mem_carrier, ContinuousLinearMap.opNorm_le_bound, TestFunction.lineDerivCLM_add, PiTensorProduct.liftEquiv_apply, HasFDerivAt.cexp, extDerivFun_zero, DoubleCentralizer.add_snd, MeasureTheory.norm_condExpInd_apply_le, LineDeriv.iteratedLineDerivOpCLM_apply, fderivWithin_iteratedFDerivWithin, fromTangentSpace_mfderiv_smul_apply', ContDiffWithinAt.clm_comp, Convex.isLittleO_alternate_sum_square, ContinuousAffineMap.decompEquiv_symm_apply, ContinuousLinearMap.rayleighQuotient_add, MultilinearMap.mkContinuousLinear_norm_le, hasFDerivAt_iff_tendsto, VonNeumannAlgebra.centralizer_centralizer, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, ContinuousLinearMap.deriv_of_bilinear, MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm, Orientation.areaForm'_apply, VectorBundleCore.coe_coordChange, hasFDerivAtFilter_iff_hasDerivAtFilter, innerSLFlip_apply_apply, ContinuousLinearMap.nnnorm_holder_apply_apply_le, ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective, Polynomial.hasFDerivAt, Distribution.mapCLM_apply, FormalMultilinearSeries.norm_compContinuousLinearMap_le, Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange, ProbabilityTheory.HasIndepIncrements.map, ContinuousLinearMap.bilinear_hasTemperateGrowth, IsBoundedBilinearMap.isBoundedLinearMap_deriv, UpperHalfPlane.smulFDeriv_J_mul, IsContinuousRiemannianBundle.exists_continuous, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, DoubleCentralizer.norm_snd, ConvexOn.sSup_of_nat_affine_eq, ContinuousLinearMap.postcomp_apply, Submodule.fst_orthogonalDecomposition_apply, LinearMap.coe_toContinuousLinearMap, ContinuousLinearMap.prodMapL_apply, ContinuousLinearMap.uncurryLeft_apply, hasFDerivWithinAt_one, Bundle.Trivialization.symmL_continuousLinearMapAt, ContinuousLinearMap.antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range, ContinuousLinearMap.toSpanSingletonLE_apply, ContinuousLinearEquiv.nhds, Submodule.smul_starProjection_singleton, ContinuousLinearMap.map_smulₛₗ, ContinuousLinearMap.opNorm_comp_le, DoubleCentralizer.nnnorm_fst, ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap, intervalIntegral.integral_hasStrictFDerivAt, fderivWithin_mul_const', ContinuousAlternatingMap.curryLeft_compContinuousLinearMap, IsBilinearMap.toContinuousBilinearMap_apply, MDifferentiableWithinAt.clm_apply_of_inCoordinates, TestFunction.lineDerivOp_eq_lineDerivCLM, Complex.ofRealCLM_apply, contMDiffOn_continuousLinearMapCoordChange, fderivWithin_smul, ContinuousLinearMap.instCompleteSpace, InnerProductSpace.enorm_rankOne, Module.Basis.exists_opNNNorm_le, InnerProductSpace.continuousLinearMapOfBilin_zero, differentiableAt_complex_iff_differentiableAt_real, mfderiv_coe_sphere_injective, ContinuousMultilinearMap.compContinuousLinearMapLRight_apply, PiTensorProduct.mapL_mul, cfcHom_real_eq_restrict, ContinuousLinearMap.toLinearMap_innerSL_apply, SchwartzMap.fourierMultiplierCLM_apply, SchwartzMap.pderivCLM_apply, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, hasFDerivAt_ofNat, hasFDerivAt_list_prod_finRange', ContinuousMultilinearMap.apply_apply, ContDiff.smulRight, ContinuousMultilinearMap.flipLinear_apply_apply, Submodule.starProjection_norm_le, HasStrictFDerivAt.neg, WeakDual.CharacterSpace.coe_toCLM, mfderiv_add, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, RKHS.inner_kerFun, CStarMatrix.toCLM_apply_single, Real.fourier_fderiv, ContinuousLinearMap.lipschitzWith_of_opNorm_le, Submodule.inner_orthogonalProjection_eq_of_mem_right, Continuous.continuousLinearMapCoprod, ContinuousLinearMap.isLeast_opNNNorm, ContinuousAffineMap.linear_decompAffineEquiv, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one, IsSelfAdjoint.spectrumRestricts, hasFTaylorSeriesUpTo_succ_nat_iff_right, IsCovariantDerivativeOn.leibniz, hasFDerivWithinAt_zero, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, HasFDerivWithinAt.norm_sq, MeasureTheory.norm_weightedSMul_le, lp.singleContinuousLinearMap_apply, Complex.restrictScalars_one_smulRight, MDifferentiableAt.clm_comp, HasDerivAt.clm_comp, ProbabilityTheory.HasGaussianLaw.map, norm_fderiv_norm_rpow_le, ContinuousMultilinearMap.toContinuousLinearMap_apply, SeparationQuotient.exists_out_continuousLinearMap, ContinuousLinearMap.one_apply, StrongDual.dualPairing_separatingLeft, VectorFourier.fderiv_fourierIntegral, ContinuousLinearMap.uncurryBilinear_apply, VectorBundle.continuousOn_coordChange', ContinuousLinearMap.rayleighQuotient_le_of_norm_mem_resolventSet, ContinuousLinearMap.mfderiv_eq, MeasureTheory.integral_posConvolution, hasFDerivWithinAt_singleton, ContinuousAffineMap.contLinear_eq_zero_iff_exists_const, SchwartzMap.fourierInv_lineDerivOp_eq, VectorFourier.integral_fourierIntegral_swap, NormedSpace.inclusionInDoubleDualWeak_apply, Bundle.RiemannianMetric.symm, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, HasStrictFDerivAt.add, LinearMap.toContinuousLinearMap_eq_iff_eq_toLinearMap, MDifferentiableOn.clm_bundle_apply, Unitization.norm_eq_sup, ContinuousWithinAt.clm_apply, ProbabilityTheory.isGaussian_map, ContinuousMap.toLp_norm_eq_toLp_norm_coe, Matrix.ofLp_toEuclideanCLM, hasFTaylorSeriesUpToOn_succ_nat_iff_right, ContinuousLinearMap.coe_add', CStarMatrix.toCLM_apply_eq_sum, ContinuousLinearMap.le_of_opNorm_le, Submodule.norm_starProjection, fderiv_cos, MeasureTheory.weightedSMul_add_measure, Unitary.linearIsometryEquiv_coe_symm_apply, Submodule.eq_starProjection_of_mem_of_inner_eq_zero, ContDiff.comp_continuousLinearMap, MeasureTheory.Measure.map_conv_continuousLinearMap, hasFDerivWithinAt_comp_smul_smul_iff, ContinuousLinearMap.coeLM_apply, banach_steinhaus, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fourierCoeff_toLp, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply, ContinuousLinearMap.rayleighQuotient_le_norm, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst, LinearMap.isPositive_toContinuousLinearMap_iff, ContinuousLinearMap.norm_def, ProbabilityTheory.variance_continuousLinearMap_gaussianReal, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', fderivWithin_zero_of_notMem_closure, ContinuousLinearMap.le_opNorm_of_le, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, curveIntegral_fun_add, ContinuousLinearEquiv.lipschitz, iteratedDeriv_vcomp_three, VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt, fderivWithin_fun_pow, RCLike.sqrt_map, Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff, iteratedFDerivWithin_two_apply', HasStrictFDerivAt.arctan, curveIntegral_fun_neg, HasFDerivAtFilter.const_smul, TopModuleCat.hom_id, ContinuousLinearMap.opNNNorm_le_bound', NormedSpace.equicontinuous_TFAE, ContinuousLinearMap.differentiable, Submodule.starProjection_map_apply, IsMIntegralCurveAt.hasMFDerivAt, HasFDerivAt.multiset_prod, extDerivFun_add, SpectrumRestricts.real_iff, TrivSqZeroExt.inrCLM_apply, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, HasFDerivAt.mul_const, Bundle.Pretrivialization.continuousLinearMap_symm_apply, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, ContinuousLinearMap.opNorm_add_le, ContinuousLinearMap.sSup_sphere_eq_norm, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, DoubleCentralizer.neg_toProd, FormalMultilinearSeries.radius_unshift, HasFPowerSeriesAt.fderiv_eq, hasStrictFDerivAt_zero, ContDiffPointwiseHolderAt.continuousLinearMap_comp, ContinuousLinearMap.coe_restrictScalarsIsometry, ContinuousLinearMap.memLp_of_bilin, SchauderBasis.exists_norm_proj_le, ContinuousLinearMap.norm_inr, ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap, SchwartzMap.smulLeftCLM_smulLeftCLM_apply, Submodule.starProjection_bot, VectorField.mlieBracketWithin_smul_left, ContinuousLinearMap.isometry_iff_adjoint_comp_self, ContinuousLinearMap.differentiableWithinAt, HasFDerivWithinAt.mapsTo_tangent_cone, PiTensorProduct.dualSeminorms_bounded, HasFDerivWithinAt.mul_const', HasDerivAt.comp_hasFDerivWithinAt_of_eq, ContinuousLinearMap.postcompCompactConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, ProbabilityTheory.covarianceBilin_self_nonneg, HasStrictFDerivAt.iterate, ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm, ContinuousLinearMap.opNorm_extend_le, IsSelfAdjoint.conj_adjoint, ContinuousLinearMap.compLeftContinuous_apply, ContinuousMultilinearMap.curryMidEquiv_apply, complexOfReal_deriv, fderiv_const_mul, ApproximatesLinearOn.lipschitz_sub, HasStrictFDerivAt.continuousMultilinear_apply_const, ContinuousLinearMap.opNorm_mulLeftRight_apply_le, ContinuousLinearMap.analyticOnNhd_bilinear, ContinuousLinearMap.reApplyInnerSelf_apply, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', fderiv_exp, DoubleCentralizer.algebraMap_snd, UnconditionalSchauderBasis.norm_proj_le_nnnormProjBound, ContinuousLinearMap.differentiableAt, ContinuousLinearMap.sub_apply, fderiv_arctan, fderivWithin_const, ProbabilityTheory.covarianceBilinDual_self_eq_variance, LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply, SchauderBasis.RankOneDecomposition.basisCoeff_spec, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, iteratedFDerivWithin_succ_apply_left, HasFDerivAtFilter.fun_const_smul, hasStrictFDerivAt_norm_sq, Submodule.starProjection_unit_singleton, CovariantDerivative.zero, fderiv_tsum, SchwartzMap.fourier_evalCLM_eq, ContinuousLinearEquiv.equivOfInverse_apply, DoubleCentralizer.one_snd, LinearMap.compLeftInverse_apply_of_bdd, ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, contDiffOn_infty_iff_fderiv_of_isOpen, fderiv_pow_ring', ContinuousLinearMap.map_sub₂, QuasispectrumRestricts.real_iff, ContinuousLinearMap.bilinearComp_apply, fderiv_natCast, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le, LinearEquiv.extendOfIsometry_apply, SchwartzMap.evalCLM_apply_apply, HasFDerivAtFilter.fun_sub, ContinuousLinearMap.intrinsicStar_zero, OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective, ContinuousLinearMap.coe_pow, fderiv_const, ContMDiffWithinAt.clm_bundle_apply₂, ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply, ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousOn.prod_mapL, CStarMatrix.toCLM_apply, RKHS.coeCLM_injective, DoubleCentralizer.algebraMap_toProd, ContinuousLinearMap.sub_comp, SeparationQuotient.mk_outCLM, ContinuousLinearMap.ker_self_comp_adjoint, fderivWithin.log, ContinuousLinearMap.norm_map_tail_le, contMDiffOn_symm_coordChangeL, ContinuousAffineMap.map_vadd, ContinuousLinearMap.instStarModuleId, Polynomial.hasFDerivAt_aeval, contMDiffAt_hom_bundle, ContinuousAt.continuousLinearMapCoprod, VectorField.mlieBracketWithin_smul_right, ContinuousLinearMap.compContinuousAlternatingMap_coe, ContinuousLinearMap.compContinuousMultilinearMap_coe, HasFDerivAt.continuousAlternatingMap_apply_const, PiTensorProduct.injectiveSeminorm_apply, ContinuousLinearMap.isBoundedLinearMap_comp_left, FormalMultilinearSeries.compContinuousLinearMap_applyComposition, MeasureTheory.MemLp.continuousLinearMap_comp, norm_fderiv_iteratedFDeriv, curveIntegralFun_neg, TestFunction.lineDerivCLM_eq_fderivCLM, MeasureTheory.Lp.norm_constL_le, ProbabilityTheory.covarianceBilinDual_self_nonneg, conformalFactorAt_inner_eq_mul_inner', ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply, hasFDerivAt_pow, ProbabilityTheory.isGaussian_map_of_measurable, TemperedDistribution.fourier_lineDerivOp_eq, ContDiffPointwiseHolderAt.clm_apply, Matrix.l2_opNNNorm_def, hasMFDerivAt_const, VonNeumannAlgebra.IsIdempotentElem.mem_iff, MeasureTheory.L1.SimpleFunc.setToL1S_const, LinearMap.extendOfNorm_eq, ContinuousLinearMap.integrable_comp, ContinuousLinearMap.adjointAux_adjointAux, HasStrictFDerivAt.const_sub, GeneralSchauderBasis.proj_empty, fderiv_sub, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, TopModuleCat.freeMap_map, Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl, ContDiffOn.clm_comp, hasFDerivAt_single, ContMDiffAt.clm_precomp, MeasureTheory.condExpL2_indicator_of_measurable, TestFunction.lineDerivCLM_apply, ProbabilityTheory.covarianceBilin_real_self, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, PositiveLinearMap.gnsStarAlgHom_apply, ContDiffOn.continuousOn_fderivWithin_apply, HasFDerivWithinAt.iterate, MeasureTheory.condExp_ae_eq_condExpL1CLM, HasMFDerivWithinAt.sum, LinearEquiv.extend_symm_apply, ContinuousLinearMap.integral_comp_id_comm', ContinuousLinearMap.coprodEquivL_apply_apply, ContinuousLinearMap.intrinsicStar_eq_comp, HasFTaylorSeriesUpToOn.hasFDerivAt, LinearIsometry.norm_toContinuousLinearMap_comp, BoundedContinuousFunction.coeFn_toLp, ContinuousLinearMap.isBigOWith_comp, ContinuousLinearMap.flip_add, MDifferentiable.clm_prodMap, continuous_clm_apply, ContinuousLinearEquiv.skewProd_apply, ContinuousLinearMap.hasTemperateGrowth, VectorFourier.fourierSMulRight_apply, ContinuousLinearMap.isSelfAdjoint_iff', DoubleCentralizer.pow_toProd, measurable_fderiv_apply_const, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, ContinuousLinearMap.toContinuousAddMonoidHom_injective, isSelfAdjoint_starProjection, InnerProductSpace.gramSchmidt_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, VectorBundleCore.localTriv_coordChange_eq, ContinuousMultilinearMap.uncurryRight_apply, MeasureTheory.L1.tendsto_setToL1, eventually_norm_symmL_trivializationAt_self_comp_lt, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le', ContinuousLinearMap.isVonNBounded_iff, MeasureTheory.condExpL1CLM_indicatorConst, SchwartzMap.fourierMultiplierCLM_ofReal, mfderivWithin_zero_of_not_mdifferentiableWithinAt, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, differentiableWithinAt_iff_restrictScalars, ContDiffWithinAt.comp_continuousLinearMap, MeasureTheory.L1.nnnorm_Integral_le_one, ContDiffWithinAt.laplacianWithin_CLM_comp_left, Manifold.riemannianEDist_def, HasFDerivAtFilter.isLittleO, ContinuousLinearMap.range_coeFn_eq, curveIntegralFun_fun_zero, ContinuousLinearMap.bilinearComp_zero, HasFDerivAt.fun_pow', ContinuousLinearMap.isVonNBounded_image2_apply, SchwartzMap.smulLeftCLM_add, MeasureTheory.weightedSMul_smul, HasMFDerivWithinAt.mul', ContinuousLinearEquiv.norm_symm_pos, MeasureTheory.integral_continuousLinearMap_prod, MultilinearMap.mkContinuousLinear_norm_le', ContinuousLinearMap.NonlinearRightInverse.right_inv, norm_fderivWithin_iteratedFDerivWithin, HasFTaylorSeriesUpToOn.shift_of_succ, ContinuousLinearMap.inverse_zero, curveIntegralFun_def', contDiffOn_fderiv_coord_change, HasFDerivAtFilter.fun_add, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2, ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, HasFDerivWithinAt.hasDerivWithinAt, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, HasGradientWithinAt.fderivWithin_apply, ContMDiffOn.clm_apply, Algebra.IsCentral.instContinuousLinearMap, MeasureTheory.L1.setToL1_unique, ContinuousLinearMap.restrictScalars_sub, cfc_eq_cfcL_mkD, norm_derivWithin_eq_norm_fderivWithin, ApproximatesLinearOn.antilipschitz, ContinuousLinearMap.le_def, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, contDiff_succ_iff_fderiv_apply, VectorBundleCore.localTriv_apply, fderiv_ccos, DoubleCentralizer.zero_fst, ContinuousLinearMap.default_def, LinearIsometryEquiv.coe_coe'', NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, ContinuousAffineMap.decompAffineEquiv_symm_apply, fderiv_update, RKHS.coeCLM_apply, ContinuousLinearMap.IsPositive.re_inner_nonneg_left, ProbabilityTheory.HasGaussianLaw.map_of_measurable, extDerivWithin_apply_vectorField, ContinuousLinearMap.measurable_comp, Real.fourier_bilin_convolution_eq, BoxIntegral.BoxAdditiveMap.toSMul_apply, ProbabilityTheory.IsGaussian.map_rotation_eq_self, ContinuousLinearMap.hasFDerivWithinAt, IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt, CStarMatrix.mul_entry_mul_eq_inner_toCLM, hom_trivializationAt, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, ContinuousLinearMap.le_opNorm₂, ContinuousLinearMap.lpPairing_eq_integral, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, ContinuousLinearMap.norm_iteratedFDeriv_comp_left, LinearMap.clmOfExistsBoundedImage_apply, ContinuousLinearMap.norm_uncurryMid, ProbabilityTheory.covarianceOperator_inner, InnerProductSpace.rankOne_def', ContDiff.clm_comp, ContDiff.fderiv_apply, ContinuousLinearMap.opNorm_mul_le, ContinuousLinearMap.uncurryLeft_norm, ContDiffWithinAt.fderivWithin', ContinuousLinearMap.opNorm_subsingleton, HasFDerivAt.comp_hasDerivWithinAt, Filter.EventuallyEq.fderiv, HasFDerivWithinAt.multilinear_comp, ContinuousLinearEquiv.coe_injective, fderiv_apply_one_eq_deriv, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id, MDifferentiableAt.clm_apply_of_inCoordinates, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, HasFTaylorSeriesUpToOn.compContinuousLinearMap, hasFDerivAt_zero_of_eventually_const, SchwartzMap.fourierMultiplierCLM_const, ContDiffOn.continuousOn_fderivWithin, SchwartzMap.integral_sesq_fourierIntegral_eq, Submodule.norm_orthogonalProjection_apply, contDiffAt_succ_iff_hasFDerivAt, fderivWithin_const_smul_of_invertible, ContinuousLinearMap.IsPositive.inner_nonneg_left, ContinuousLinearMap.map_add, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, TestFunction.monoCLM_eq_of_scalars, hasFDerivAt_const, ContinuousLinearMap.coe_copy, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left', fderiv_continuousMultilinear_apply_const_apply, MeasureTheory.Integrable.convolution_integrand, MeasureTheory.condExpL1CLM_lpMeas, fderivWithin_exp, ProbabilityTheory.HasGaussianLaw.map_fun, ContMDiffWithinAt.clm_bundle_apply, Submodule.eq_starProjection_of_mem_orthogonal, Differentiable.clm_apply, ContinuousLinearMap.mdifferentiableWithinAt, SeparatingDual.completeSpace_continuousLinearMap_iff, ContMDiff.clm_bundle_apply, ProbabilityTheory.covarianceBilin_apply_pi, HasStrictFDerivAt.fun_sub, SchwartzMap.integral_bilinear_laplacian_right_eq_left, ContinuousLinearMap.natCast_apply, HasFDerivAt.lim, ContinuousLinearMap.isometry_mul, ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range, ContinuousLinearMap.isOpen_injective, HasFDerivAt.const_mul, MeasureTheory.L1.setToL1_apply_coeToLp, HasStrictFDerivAt.isEquivalent_sub, HasStrictFDerivAt.continuousAlternatingMap_apply, ContinuousAffineMap.add_contLinear, DoubleCentralizer.sub_toProd, ContinuousLinearMap.continuous_uncurry_of_multilinear, Complex.conjCLE_nnorm, tendsto_iff_forall_eval_tendsto_topDualPairing, HasStrictDerivAt.complexToReal_fderiv', LinearIsometry.map_starProjection, ContinuousLinearMap.inr_apply, MeasureTheory.dist_convolution_le', fderivWithin_multiset_prod, ContinuousLinearMap.isInducing_postcomp, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, HasFDerivAt.mul, ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff, Asymptotics.IsBigO.hasFDerivWithinAt, LinearMap.opNorm_extendOfNorm_le, Continuous.prod_map_equivL, CovariantDerivative.torsion_eq_zero_iff, MeasureTheory.integral_continuousLinearMap_prod', ConvexOn.real_univ_sSup_affine_eq, DifferentiableWithinAt.clm_comp, MeasureTheory.weightedSMul_union, MDifferentiableOn.cle_arrowCongr, InnerProductSpace.innerSL_norm, hasFDerivAt_exp_zero, ContinuousLinearMap.toSpanSingleton_one, fderiv_add, SchauderBasis.proj_comp, DoubleCentralizer.nnnorm_fst_eq_snd, Unitization.norm_def, ContMDiff.clm_bundle_apply₂, VonNeumannAlgebra.IsStarProjection.mem_iff, MeasureTheory.L1.setToL1_congr_left', ContinuousLinearMap.measurable_apply, SeparationQuotient.postcomp_mkCLM_surjective, fderivWithin_neg, hasFDerivAtFilter_iff_isLittleOTVS, ContinuousMultilinearMap.norm_ofSubsingleton_id_le, second_derivative_symmetric, ContinuousAlternatingMap.curryLeft_same, ContinuousMultilinearMap.curryRight_apply, Distribution.dsupport_smulLeftCLM_subset, Submodule.inner_orthogonalProjection_eq_of_mem_left, ContMDiffWithinAt.mfderivWithin, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, Bundle.Trivialization.baseSet_continuousLinearMap, eventually_norm_symmL_trivializationAt_comp_self_lt, ContinuousLinearMap.IsPositive.add, MeasureTheory.SimpleFunc.setToSimpleFunc_indicator, HasFDerivAt.comp_hasDerivWithinAt_of_eq, CurveIntegrable.fun_neg, ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds, mfderivWithin_const, hasStrictFDerivAt_pow', ContinuousLinearMap.applySMulCommClass, ContinuousLinearMap.norm_single, VectorPrebundle.exists_coordChange, DoubleCentralizer.one_fst, ContinuousLinearMap.continuous, MDifferentiableOn.clm_apply, fderivWithin_eventually_congr_set, MDifferentiableAt.clm_precomp, MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral, ContDiffMapSupportedIn.postcompCLM_apply, SchwartzMap.compSubConstCLM_comp, TemperedDistribution.smulLeftCLM_add, ContinuousAlternatingMap.curryLeft_zero, IsContDiffImplicitAt.bijective, Submodule.eq_starProjection_of_mem_orthogonal', ProbabilityTheory.covarianceBilin_apply_basisFun, ContinuousLinearMap.coe_piMap', ContinuousMultilinearMap.analyticOn_uncurry_of_linear, fderivWithin_fun_const, Complex.restrictScalars_toSpanSingleton, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, ContinuousLinearMap.opENorm_comp_le, algebraMapCLM_apply, curveIntegrable_neg_iff, hasMFDerivWithinAt_const, iteratedFDeriv_one_apply, hasFDerivAt_exp_smul_const_of_mem_ball, fderiv_fun_mul', ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft, HasFDerivAt.const_smul, HasFDerivAt.hasLineDerivAt, MeasureTheory.L1.setToL1_congr_left, ContinuousLinearMap.adjoint_comp_self_injective_iff, iteratedFDeriv_succ_apply_right, FormalMultilinearSeries.leftInv_coeff_one, ContinuousLinearMap.hasMFDerivAt, mdifferentiableOn_continuousLinearMapCoordChange, TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, ContDiffMapSupportedIn.fderivCLM_eq_of_scalars, fderiv_deriv, ContDiffAt.hasStrictFDerivAt_implicitFunction, MeasureTheory.L1.setToL1_smul, ContinuousLinearEquiv.coe_apply, HasFDerivAtFilter.add, HasFDerivAt.lim_real, PointwiseConvergenceCLM.precomp_apply, ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, ContinuousLinearMap.toContinuousAddMonoidHom_inj, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, InnerProductSpace.isStarProjection_rankOne_self, SeparationQuotient.mk_comp_outCLM, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, contDiff_clm_apply_iff, HasFPowerSeriesAt.hasFDerivAt, norm_fderiv_norm, eventually_enorm_mfderiv_extChartAt_lt, ContinuousLinearMap.restrictScalars_zero, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, hasFDerivAt_exp_smul_const, ContinuousLinearMap.hasStrictFDerivAt, LinearMap.mkContinuous₂_norm_le, ContinuousLinearMap.instNontrivialId, MeasureTheory.AEStronglyMeasurable.fourierSMulRight, oneTangentSpaceIcc_def, TrivSqZeroExt.inlCLM_apply, ContinuousLinearMap.hasFPowerSeriesAt_bilinear, ContinuousLinearMap.comp_analyticOn, ContinuousLinearMap.continuousConstSMul, fderiv_finset_prod, ContinuousLinearMap.self_comp_adjoint_injective_iff, Bundle.Trivialization.continuousLinearMapAt_apply, ContinuousLinearMap.coeFn_compLpL, hasStrictFDerivAt_list_prod_attach', Real.Lp.fourierTransformCLM_apply, ContinuousLinearMap.sub_apply', ContinuousLinearMap.coeFn_injective, DoubleCentralizer.sub_fst, contDiffOn_clm_apply, ContinuousLinearMap.le_opNNNorm, Bundle.Trivialization.symmL_apply, ContinuousLinearMap.restrictScalars_smul, fderiv_continuousAlternatingMap_apply_apply, Submodule.starProjection_orthogonal, PiTensorProduct.mapLMultilinear_apply_apply, ContinuousLinearMap.instNonnegSpectrumClassRealId, ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint, HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq, HasFDerivWithinAt.clm_comp, ContinuousLinearMap.uncurryMid_apply, ContinuousLinearMap.evalL_apply, hasFDerivAt_update, isBoundedBilinearMap_apply, AEMeasurable.apply_continuousLinearMap, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left', ContinuousLinearMap.fst_comp_inr, ContinuousLinearMap.integral_comp_commSL, RCLike.ofRealCLM_norm, ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse, Complex.sqrt_map, hasStrictFDerivAt_ringInverse, Continuous.const_clm_comp, ContDiffOn.continuousOn_fderiv_of_isOpen, ContinuousLinearMap.mul_apply', fromTangentSpace_mfderiv_smul, ContDiffOn.continuousLinearMap_comp, HasFDerivAt.fun_sum, fderiv_zero_of_not_differentiableAt, Unitary.norm_map, Submodule.starProjection_apply_mem, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, InnerProductSpace.rankOne_comp_rankOne, ContinuousLinearMap.opNorm_zero, HasStrictDerivAt.comp_hasStrictFDerivAt, HasDerivWithinAt.comp_hasFDerivWithinAt, TestFunction.mkCLM_apply, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem, SchauderBasis.proj_apply_basis_mem, BoxIntegral.hasIntegral_const, ContinuousMap.toLp_injective, TestFunction.fderivCLM_eq_of_scalars, DifferentiableAt.comp_semilinear₁, ContinuousAlternatingMap.compContinuousLinearMap_apply, ContinuousLinearMap.comp_smulₛₗ, LinearMap.mkContinuous_norm_le', DoubleCentralizer.pow_fst, PiTensorProduct.mapL_apply, MeasureTheory.integrable_continuousLinearMap_prod', hasStrictFDerivAt_finset_prod, TestFunction.lineDerivCLM_eq_of_scalars, fderiv_fun_neg, ContinuousMapZero.evalCLM_apply, isCompactOperator_of_locallyCompactSpace_rng, curveIntegral_zero, SchauderBasis.nnnorm_proj_le_nnnormProjBound, InnerProductSpace.rankOne_comp, HasDerivWithinAt.comp_hasFDerivAt, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, ContinuousLinearMap.hasBasis_nhds_zero_of_basis, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, HasFDerivAt.le_of_lip', SchwartzMap.tsupport_smulLeftCLM_subset, Real.fourierIntegral_fderiv, HasMFDerivAt.sub, InnerProductSpace.toMatrix_rankOne, MDifferentiableWithinAt.clm_comp, HasFDerivWithinAt.continuousMultilinear_apply_const, IsCovariantDerivativeOn.add, eventually_norm_symmL_trivializationAt_lt, cfcₙHom_real_eq_restrict, PiTensorProduct.liftIsometry_comp_mapL, MDifferentiableOn.clm_comp, ContinuousLinearMap.opNorm_le_iff, ContinuousLinearMap.completion_apply_coe, InnerProductSpace.isSymmetric_rankOne_self, ContinuousMap.coe_toLp, fderiv_const_sub, continuousMultilinearCurryLeftEquiv_apply, tsupport_fderiv_subset, PolynormableSpace.banach_steinhaus, SchauderBasis.RankOneDecomposition.proj_zero, ContinuousAlternatingMap.ofSubsingleton_apply_apply, HasMFDerivWithinAt.add, isStarProjection_starProjection, precomp_compactConvergenceCLM_apply, ContMDiffAt.clm_prodMap, unitary.norm_map, ContinuousAlternatingMap.restrictScalarsCLM_apply, ContMDiffWithinAt.mfderivWithin_apply, SchwartzMap.tsupport_fderivCLM_subset, ContinuousLinearMap.isBigOTVS_comp, ContinuousLinearMap.NonlinearRightInverse.right_inv', ContinuousLinearMap.restrictScalarsIsometry_toLinearMap, ContinuousLinearMap.integral_comp_L1_comm, curveIntegralFun_add, ContinuousLinearMap.opNorm_zero_iff, ContinuousLinearMap.intervalIntegral_apply, AnalyticOnNhd.fderiv, selfAdjointPartL_apply_coe, HasFDerivWithinAt.comp_hasDerivWithinAt, HasFDerivWithinAt.isEquivalent_sub, HasFDerivWithinAt.sub, HasFDerivAtFilter.fun_neg, PiTensorProduct.liftIsometry_symm_apply, fderivWithin_continuousAlternatingMap_apply_apply, SchwartzMap.smulLeftCLM_neg, ContinuousLinearMap.opNNNorm_mul, ContinuousLinearMap.ringInverse_eq_inverse, Complex.conjCLE_enorm, ContinuousLinearMap.toContinuousAddMonoidHom_neg, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear, mfderiv_zero_of_not_mdifferentiableAt, MeasureTheory.aestronglyMeasurable_condExpL1CLM, iteratedFDeriv_succ_eq_comp_right, MeasureTheory.SimpleFunc.setToSimpleFunc_zero, ContinuousLinearMap.ofNat_apply, curveIntegralFun_sub, ContDiffMapSupportedIn.seminorm_apply, ContinuousAffineMap.snd_decompLinearIsometryEquiv, DifferentiableAt.clm_comp, VectorField.lieBracket_smul_left, ContinuousLinearMap.rotation_apply, ContinuousLinearMap.coe_sum', DoubleCentralizer.algebraMap_fst, fderiv_continuousLinearEquiv_comp, nnnorm_fderiv_norm_rpow_le, hasFDerivWithinAt_natCast, ContinuousLinearMap.intrinsicStar_smulRight, deriv_clm_comp, HasStrictFDerivAt.approximates_deriv_on_open_nhds, SchwartzMap.convolution_continuous_left, ContinuousLinearMap.adjoint_toSpanSingleton, hasStrictFDerivAt_exp_zero_of_radius_pos, ContinuousLinearMap.toBilinForm_injective, ContinuousLinearMap.ext_iff, ContDiffMapSupportedIn.structureMapCLM_top_apply, ContinuousLinearMap.mfderivWithin_eq, ContinuousMultilinearMap.nnnorm_ofSubsingleton, ContDiffOn.fderivWithin, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, ContinuousLinearMap.norm_compContinuousAlternatingMap_le, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, TangentBundle.symmL_model_space, HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq, MeasureTheory.integrable_condExpL2_indicator, tangentCoordChange_self, fderiv_norm_smul, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, ContinuousLinearMap.isEmbedding_restrictScalars, spectrum.hasFDerivAt_resolvent, ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm, LinearIsometry.enorm_toContinuousLinearMap, fderivWithin_fun_add, RKHS.kerFun_inner, Bundle.Trivialization.continuousLinearMap_apply, IsBoundedBilinearMap.toContinuousLinearMap_apply, TopModuleCat.hom_sub, HasFPowerSeriesWithinOnBall.fderivWithin_eq, MeasureTheory.weightedSMul_union', hom_trivializationAt_source, ContinuousLinearMap.norm_id_le, HasFDerivAt.le_of_lipschitz, ContinuousLinearMap.ker_adjoint_comp_self, HasFDerivWithinAt.pow', SchwartzMap.pairing_continuous_left, ConvexOn.univ_sSup_affine_eq, ContinuousLinearMap.smulRight_comp_smulRight, Real.hasFDerivAt_fourierIntegral, SchwartzMap.integralCLM_apply, IsCovariantDerivativeOn.add_one_form, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, HasStrictFDerivAt.hasStrictDerivAt, ContinuousLinearMap.isScalarTower, FormalMultilinearSeries.radius_shift, hasFDerivAt_iff_isLittleOTVS, ConvexOn.real_univ_sSup_of_nat_affine_eq, fderivWithin_sqrt, fderivWithin_natCast, ContinuousLinearMap.projKerOfRightInverse_comp_inv, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, ContinuousLinearMap.neg_apply, innerSLFlip_apply, ContinuousAt.clm_bundle_apply₂, FormalMultilinearSeries.div_le_radius_compContinuousLinearMap, LinearMap.mkContinuous_norm_le, fderivWithin_derivWithin, ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars, HasFDerivAt.list_prod', ProbabilityTheory.covarianceBilin_real, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', separatingDual_iff_injective, fderivWithin_const_smul_field, fderiv_continuousMultilinearMapCompContinuousLinearMap, TopModuleCat.forget₂_TopCat_obj, ContinuousLinearMap.measurable_coe, HasFDerivAt.fun_neg, ContinuousLinearMap.analyticOn, Polynomial.fderivWithin_aeval, fderiv_sinh, ContinuousLinearMap.nndist_le_opNNNorm, MeasureTheory.L1.SimpleFunc.setToL1S_zero_left, hasFDerivAt_pow', SchwartzMap.lineDerivOp_fourierInv_eq, LinearIsometryEquiv.symm_conjStarAlgEquiv, mdifferentiableOn_coordChangeL, Polynomial.fderivWithin, LinearMap.IsContPerfPair.bijective_right, ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le, HasFDerivAt.fun_add, TopModuleCat.hom_nsmul, VectorPrebundle.mk_coordChange, ContinuousLinearMap.opNorm_lsmul_le, ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap, ContinuousLinearMap.toSpanSingleton_add, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, ProbabilityTheory.covarianceBilin_of_not_memLp, ContDiffMapSupportedIn.monoCLM_eq_zero, ContinuousAffineMap.vadd_contLinear, Matrix.linfty_opNorm_toMatrix, ConvexOn.real_sSup_of_countable_affine_eq, cfcL_integral, ContinuousMap.coeFn_toLp, MeasureTheory.L1.norm_setToL1_le_mul_norm', ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit, ContinuousLinearMap.homeomorphOfUnit_symm_apply, innerSL_apply_norm, Real.fourier_bilin_convolution_eq_integral, SeparationQuotient.liftCLM_apply, SchauderBasis.RankOneDecomposition.exists_coeff, ContinuousWithinAt.clm_bundle_apply₂, ContinuousLinearMap.isPositive_def', ContinuousLinearMap.coe_restrictScalarsL, ContinuousLinearMap.fderivWithin, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, Submodule.subtypeL_apply, ContinuousAffineMap.coe_contLinear, hasStrictFDerivAt_exp_zero, ContinuousLinearMap.norm_compL_le, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, ContMDiffVectorBundle.contMDiffOn_coordChangeL, curveIntegral_eq_intervalIntegral_deriv, Filter.EventuallyEq.fderivWithin', fderivWithin_clm_comp, ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars, ContinuousLinearMap.continuousSemilinearMapClass, lp.tsumCLM_apply, HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq, ContDiffAt.continuousLinearMap_comp, ProbabilityTheory.variance_dual_prod', HasStrictFDerivAt.fun_neg, HasFDerivWithinAt.arctan, HasStrictFDerivAt.sum, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, HasCompactSupport.fderiv_apply, fderiv_continuousMultilinear_apply_const, SchauderBasis.succSub_ortho, ProbabilityTheory.covarianceBilinDual_comm, NormedSpace.isEmbedding_inclusionInDoubleDualWeak, ContinuousLinearMap.opNNNorm_mul_flip_apply, ContinuousLinearMap.compLeftContinuousBounded_apply, ContinuousLinearMap.norm_fst, HasFPowerSeriesOnBall.hasFDerivAt, CovariantDerivative.torsion_antisymm, ContinuousLinearMap.opNNNorm_comp_le, Submodule.starProjection_orthogonalComplement_singleton_eq_zero, HasMFDerivAt.prod, ContMDiffWithinAt.clm_apply_of_inCoordinates, fderivWithin_csin, ContinuousMultilinearMap.curryMid_apply, ContinuousLinearMap.comp_zero, PiTensorProduct.mapL_opNorm, HasFDerivWithinAt.comp_hasDerivAt, SchwartzMap.compCLM_apply, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le, TemperedDistribution.fourierMultiplierCLM_apply_apply, intervalIntegral.fderivWithin_integral_of_tendsto_ae, hasStrictFDerivAt_one, ContinuousMap.toLp_comp_toContinuousMap, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, ContinuousLinearEquiv.arrowCongrEquiv_symm_apply, DoubleCentralizer.mul_fst, ContMDiff.clm_postcomp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure, MDifferentiableAt.coordChangeL, fderivWithin_continuousAlternatingMap_apply_const, ContDiffAt.clm_comp, ContinuousLinearMap.norm_restrictScalars, ApproximatesLinearOn.closedBall_subset_target, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, ContinuousLinearEquiv.arrowCongrSL_apply, MDifferentiableWithinAt.clm_postcomp, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, ContinuousLinearMap.toContinuousAddMonoidHom_id, ContMDiff.clm_prodMap, IsSelfAdjoint.conj_starProjection, hasFDerivAt_natCast, ContinuousLinearMap.opNorm_mul_apply_le, hasFDerivAt_intCast, intervalIntegral.integral_hasFDerivWithinAt, ContinuousLinearMap.smul_def, ContinuousLinearMap.orthogonal_range, contDiff_one_iff_hasFDerivAt, Submodule.lipschitzWith_starProjection, MDifferentiableWithinAt.clm_bundle_apply, ContinuousLinearMap.isPositive_iff_complex, ContinuousLinearMap.toContinuousAddMonoidHom_sub, ContinuousAffineMap.snd_decompEquiv, ProbabilityTheory.covarianceBilin_apply, ContinuousLinearMap.isThetaTVS_comp, ContinuousLinearMap.neg_comp, BoxIntegral.integralSum_sub_partitions, ContinuousLinearMap.comp_cpolynomialOn, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, ContinuousLinearMap.opNorm_smul_le, MeasureTheory.L1.norm_setToL1_le', TestFunction.fderivCLM_apply_of_gt, IsBoundedBilinearMap.deriv_apply, fderiv_zero, ContinuousLinearMap.IsIdempotentElem.commute_iff, ContinuousLinearMap.spectralRadius_eq_nnnorm, TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, EuclideanGeometry.hasFDerivAt_inversion, ContinuousLinearEquiv.skewProd_symm_apply, MeasureTheory.convolutionExistsAt_iff_integrable_swap, ContinuousLinearMap.intrinsicStar_comp', norm_iteratedFDeriv_one, hasFDerivAt_tsum, ContinuousLinearMap.spectrum_eq, HasStrictFDerivAt.fun_const_smul, ContinuousLinearMap.intrinsicStar_id, StronglyMeasurable.apply_continuousLinearMap, HasFDerivAt.hasDerivAt, fderivWithin_const_smul, ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal, ContinuousLinearMap.isPositive_iff, TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, ContinuousMultilinearMap.compContinuousLinearMapL_apply, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, ContinuousLinearMap.IsInvertible.inverse_apply_self, HasFDerivWithinAt.unique_on, VectorField.pullbackWithin_eq, ContinuousLinearMap.norm_bilinearRestrictScalars, ContinuousLinearMap.nhds_zero_eq, PiTensorProduct.liftIsometry_apply_apply, ContinuousLinearMap.norm_inl, ContinuousLinearMap.coeLMₛₗ_apply, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, ProbabilityTheory.covarianceBilin_map, Unitization.nnnorm_eq_sup, SchwartzMap.fourierTransformCLM_apply, norm_deriv_eq_norm_fderiv, skewAdjointPartL_apply_coe, DoubleCentralizer.zero_toProd, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, ContinuousLinearMap.inverse_of_not_isInvertible, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, ContinuousLinearMap.bilinearComp_zero_left, ContinuousLinearMap.nnnorm_smulRight_apply, MeasureTheory.Lp.constL_apply, SchwartzMap.fderivCLM_fourier_eq, HasFDerivWithinAt.isLittleOTVS, Bundle.ContinuousRiemannianMetric.pos, SchwartzMap.derivCLM_apply, ContDiffAt.fderiv, Matrix.toLin_finTwoProd_toContinuousLinearMap, RCLike.map_nonneg_iff, IsCoercive.continuousLinearEquivOfBilin_apply, LinearMap.toContinuousLinearMap₁_apply, VectorBundleCore.continuousOn_coordChange, ContinuousLinearMap.projKerOfRightInverse_apply_idem, TemperedDistribution.fourierTransformCLM_apply, mfderiv_comp_apply, TopModuleCat.cokerπ_surjective, Unitary.inner_map_map, MDifferentiableOn.clm_precomp, HasFDerivWithinAt.fun_sum, VectorField.lieBracketWithin_smul_right, isCompactOperator_of_tendsto, fderiv_fun_const_smul, inner_gradientWithin_left, ContinuousLinearMap.adjoint_comp, ContinuousAffineMap.decompLinearEquiv_symm_apply, tsupport_fderiv_apply_subset, isConformalMap_iff, ContDiff.clm_apply, VectorFourier.integral_bilin_fourierIntegral_eq_flip, ContinuousLinearMap.coe_neg, deriv_clm_apply, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, ContinuousMultilinearMap.ofSubsingleton_apply_apply, ContinuousLinearMap.add_compLp, contDiffOn_succ_iff_fderivWithin, ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right, InnerProductSpace.toLinearMap_rankOne, instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, ContinuousLinearMap.coe_codRestrict_apply, ContinuousLinearMap.adjointAux_inner_right, hasFDerivWithinAt_ofNat, ContinuousLinearMap.isCompact_closure_image_coe_of_bounded, VectorField.mpullback_mfderivWithin_apply_smul, Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real, HasMFDerivWithinAt.mul, Bundle.RiemannianMetric.pos, ContinuousLinearEquiv.isOpen, HasStrictFDerivAt.clm_apply, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, ContMDiffAt.clm_bundle_apply₂, ContDiffMapSupportedIn.fderivLM_apply, ContinuousLinearMap.extend_zero, fderivWithin_sub, continuousMultilinearCurryRightEquiv_symm_apply', MeasureTheory.condExpInd_smul', ContinuousLinearMap.isBigO_sub, IsCovariantDerivativeOn.zero, ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, DoubleCentralizer.norm_fst, LinearMap.norm_extendOfNorm_apply_le, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, MeasureTheory.L1.setToL1_add_left, ContDiffWithinAt.fderivWithin, ContinuousLinearMap.opNNNorm_eq_of_bounds, ContinuousLinearMap.prodL_apply, ContinuousLinearEquiv.arrowCongrEquiv_apply, ContinuousLinearMap.antilipschitz_of_bound, ContinuousAlternatingMap.norm_ofSubsingleton_id, LinearMap.isStarProjection_toContinuousLinearMap_iff, Manifold.pathELength_eq_lintegral_mfderiv_Icc, IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn, TensorialAt.mkHom_apply, HasFDerivAtFilter.isLittleOTVS, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, HasFDerivAt.const_sub, ContinuousAffineMap.contLinear_map_vsub, dimH_orthogonalProjection_le, LinearIsometry.toContinuousLinearMap_injective, BoundedContinuousFunction.toLp_norm_le, iteratedFDerivWithin_two_apply, fderiv_ccosh, ContDiffMapSupportedIn.seminorm_postcompLM_le, ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap, DoubleCentralizer.coe_fst, HasStrictFDerivAt.fun_smul, hasStrictFDerivAt_ofNat, ContinuousLinearMap.coprod_apply, ContinuousLinearMap.coe_fst', ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, ContDiffPointwiseHolderAt.fderiv, fderiv_fun_mul, curveIntegral_fun_sub, ContinuousLinearMap.HasLeftInverse.isClosed_range, Submodule.re_inner_starProjection_nonneg, Submodule.adjoint_orthogonalProjection, HasFDerivAt.pow', HasStrictFDerivAt.pow', OrthogonalFamily.sum_projection_of_mem_iSup, Real.fourierIntegral_continuousLinearMap_apply', CurveIntegrable.smul, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, TopModuleCat.hom_smul, ContinuousLinearMap.hasFDerivAt_of_bilinear, Submodule.id_eq_sum_starProjection_self_orthogonalComplement, contDiffOn_succ_iff_fderiv_apply, FormalMultilinearSeries.ofScalars_comp_neg_id, ProbabilityTheory.uncenteredCovarianceBilin_zero, HasStrictFDerivAt.multiset_prod, OpenPartialHomeomorph.MDifferentiable.mfderiv_injective, VonNeumannAlgebra.coe_toStarSubalgebra, MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter, ContDiffMapSupportedIn.continuous_iff_comp_order_le, TensorialAt.mkHom₂_apply, ContinuousAlternatingMap.curryLeft_add, hasFDerivAt_integral_of_dominated_of_fderiv_le, TensorialAt.mkHom_apply_eq_extend, ContinuousLinearMap.coe_sub, Submodule.starProjection_orthogonal_apply_eq_zero, VectorFourier.fourierPowSMulRight_apply, HasFDerivWithinAt.smul, extDeriv_apply_vectorField_of_pairwise_commute, Matrix.linfty_opNorm_eq_opNorm, ContMDiffWithinAt.clm_apply, mfderivWithin_eventually_congr_set, ContinuousLinearMap.coe_restrictScalars', norm_fderiv_le_of_lipschitzOn, ContinuousLinearMap.isBoundedLinearMap, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, ContinuousLinearMap.opNorm_le_iff_lipschitz, CPolynomialOn.fderiv, ContinuousLinearMap.opNNNorm_le_of_lipschitz, ContinuousLinearMap.norm_pi_le_of_le, SchwartzMap.convolution_flip, MeasureTheory.L1.norm_setToL1_le_mul_norm, ContinuousLinearMap.opNorm_le_of_nhds_zero, ContinuousLinearMap.opNorm_flip, IsLocalMaxOn.fderivWithin_eq_zero, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, ContinuousLinearMap.precompCompactConvergenceCLM_apply, VectorPrebundle.continuousOn_coordChange, VectorField.mpullbackWithin_apply, FormalMultilinearSeries.radius_compContinuousLinearMap_le, HasStrictFDerivAt.mul_const', ContinuousLinearMap.IsPositive.adjoint_conj, ContinuousLinearMap.coe_snd', measurable_fderiv_with_param, mfderiv_const, IsConformalMap.smul, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left', IsCompactOperator.comp_clm, SchwartzMap.lineDerivOp_apply_eq_fderiv, ContinuousLinearMap.abs_rayleighQuotient_le_of_norm_mem_resolventSet, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub, ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq, conformalFactorAt_inner_eq_mul_inner, ContinuousLinearMap.exist_extension_of_finiteDimensional_range, TemperedDistribution.fourierMultiplierCLM_sum, ContMDiffCovariantDerivativeOn.contMDiff, RKHS.kernel_inner, BoxIntegral.integral_const, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, FormalMultilinearSeries.derivSeries_eq_zero, ContinuousLinearMap.differentiableOn, TestFunction.lineDerivCLM_smul, ContinuousLinearMap.isPositive_iff', ContDiffWithinAt.smulRight, ContinuousLinearMap.star_eq_adjoint, TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj, Complex.imCLM_nnnorm, ProperCone.mem_comap, ContinuousMultilinearMap.curryLeft_apply, ContDiffAt.laplacian_CLM_comp_left_nhds, Submodule.lipschitzWith_orthogonalProjection, ContMDiffWithinAt.coordChangeL, Polynomial.hasFDerivWithinAt_aeval, measurableSet_of_differentiableAt_of_isComplete_with_param, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, ContinuousLinearMap.opNorm_le_of_shell, TopModuleCat.kerι_apply, fderiv_sqrt, ContinuousLinearMap.inverse_eq_ringInverse, MeasureTheory.Integrable.apply_continuousLinearMap, ContinuousLinearMap.coe_prodMap', UniformSpace.Completion.coe_toComplL, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, fderivWithin_list_prod', AlternatingMap.mkContinuousLinear_norm_le, ProperCone.hyperplane_separation_of_notMem, fderiv_clm_apply, FormalMultilinearSeries.radius_le_radius_derivSeries, ContinuousAlternatingMap.curryLeftLI_apply, ContinuousLinearMap.prodEquiv_apply, ContinuousLinearMap.norm_single_le_one, HasFDerivWithinAt.fun_mul', ContinuousLinearEquiv.ofBijective_symm_apply_apply, ContinuousLinearMap.norm_compSL_le, MeasureTheory.norm_condExpInd_le, TestFunction.monoCLM_apply, ContMDiffFiberwiseLinear.locality_aux₁, HasFPowerSeriesWithinAt.unshift, SchauderBasis.enorm_proj_le_enormProjBound, hasFDerivAtFilter_iff_tendsto, ContinuousLinearMap.det_smulRight, innerSL_apply, hasStrictFDerivAt_list_prod, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, InnerProductSpace.isIdempotentElem_rankOne_self_iff, Submodule.norm_starProjection_apply, fderivWithin_continuousLinearEquiv_comp, ContinuousLinearMap.opNorm_nonneg, cfc_eq_cfcL, stereographic_apply, MeasureTheory.inner_condExpL2_eq_inner_fun, StrongDual.toLp_apply, ContinuousLinearMap.map_smul₂, ContinuousLinearMap.coe_flipₗᵢ, ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, HasFDerivAtFilter.iterate, Submodule.inner_starProjection_left_eq_right, PiLp.proj_apply, ContinuousLinearMap.normOneClass, ContinuousLinearMap.opNNNorm_subsingleton, ContMDiffAt.mfderiv, ContinuousLinearMap.IsPositive.spectrumRestricts, ContinuousLinearMap.snd_comp_inl, WeakSpace.coe_map, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, IsConformalMap.injective, Continuous.clm_bundle_apply₂, fderivWithin_const_apply, ContinuousLinearMap.opNorm_neg, MeasureTheory.condExpInd_disjoint_union_apply, fderivWithin_pow_ring', ContinuousLinearMap.analyticOn_uncurry_of_multilinear, norm_sub_le_mul_volume_of_norm_fderiv_le, continuousAt_hom_bundle, ContinuousAlternatingMap.norm_alternatizeUncurryFin_le, isStarProjection_iff_eq_starProjection_range, ContinuousLinearMap.add_compLpL, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst, IsSelfAdjoint.adjoint_conj, Bornology.IsVonNBounded.image, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left, VonNeumannAlgebra.mem_commutant_iff, exists_embedding_euclidean_of_compact, Complex.norm_fderiv_le_one_of_mapsTo_ball, ContinuousLinearMap.coe_id', ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero, VectorPrebundle.contMDiffOn_contMDiffCoordChange, Submodule.starProjection_minimal, ContinuousLinearMap.contMDiffWithinAt, IsCovariantDerivativeOn.torsion_apply_eq_extend, PiTensorProduct.mapL_pow, DoubleCentralizer.natCast_toProd, Real.differentiable_fourierChar_neg_bilinear_right, OrthonormalBasis.sum_rankOne_eq_id, Complex.conjCLE_norm, ContinuousLinearMap.dslope_comp, ContinuousLinearMap.inl_apply, mdifferentiableAt_coordChangeL, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, Submodule.orthogonalProjection_orthogonal_apply_eq_zero, ContinuousLinearMap.unit_le_opNorm, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le', Submodule.starProjection_mem_subspace_eq_self, MeasureTheory.L1.setToL1_zero_left', ContDiffMapSupportedIn.fderivCLM_apply_of_le, MeasureTheory.BoundedContinuousFunction.inner_toLp, ContinuousLinearMap.adjoint_inner_right, DifferentiableWithinAt.clm_apply, ContinuousLinearMap.norm_id, hasFDerivAt_integral_of_dominated_of_fderiv_le'', ContinuousMultilinearMap.nnnorm_ofSubsingleton_id, HasFDerivWithinAt.fun_pow', SeparationQuotient.isEmbedding_outCLM, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, ContDiff.contDiff_fderiv_apply, MeasureTheory.L1.norm_Integral_le_one, ContinuousLinearMap.measurable_apply', HasStrictFDerivAt.continuousAlternatingMap_apply_const, ContinuousLinearMap.toSpanSingletonLE_symm_apply, MeasureTheory.condExp_bilin_of_stronglyMeasurable_right, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt, ContDiffMapSupportedIn.postcompLM_apply, CovariantDerivative.torsion_self, DifferentiableAt.clm_apply, ContinuousLinearMap.norm_smulRightL_le, DoubleCentralizer.one_toProd, differentiableAt_iff_restrictScalars, Complex.imCLM_enorm, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, SchwartzMap.tsupport_derivCLM_subset, HasFDerivAt.comp_semilinear, ContinuousAffineMap.fst_decompLinearIsometryEquiv, MeasureTheory.integrable_continuousLinearMap_prod, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, LinearIsometryEquiv.star_eq_symm, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, ContDiffWithinAt.fderivWithin_right_apply, MeasureTheory.setToFun_const, HasFDerivWithinAt.fun_add, Bundle.Pretrivialization.continuousLinearMap_symm_apply', fderivWithin_mul_const, hasFDerivAt_zero, VectorFourier.norm_fourierSMulRight_le, continuousWithinAt_hom_bundle, ContinuousLinearMap.mul_def, UnconditionalSchauderBasis.nnnorm_proj_le_nnnormProjBound, HasFDerivAt.mul_const', ContinuousAlternatingMap.nnnorm_ofSubsingleton, MeasureTheory.charFunDual_map, HasFiniteFPowerSeriesOnBall.fderiv', ContinuousLinearMap.le_of_opNorm₂_le_of_le, ContinuousLinearMap.ofTendstoOfBoundedRange_apply, Complex.ofRealCLM_enorm, AddMonoidHom.coe_toRealLinearMap, Submodule.orthogonalProjectionFn_eq, ContinuousLinearMap.coe_sum, iteratedFDerivWithin_clm_apply_const_apply, ContinuousAlternatingMap.toContinuousLinearMap_apply, FormalMultilinearSeries.ofScalars_comp_neg, signedDist_apply, Unitization.norm_splitMul_snd_sq, HasStrictFDerivAt.fun_pow', measurable_fderiv, continuousMultilinearCurryRightEquiv_apply', ContinuousLinearMap.flipₗᵢ'_symm, TemperedDistribution.lineDerivOp_fourierInv_eq, AnalyticAt.compContinuousLinearMap, DoubleCentralizer.natCast_snd, VonNeumannAlgebra.coe_commutant, mfderiv_smul, HasFiniteFPowerSeriesOnBall.hasFDerivAt, ProbabilityTheory.variance_dual_prod, TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, ContinuousAlternatingMap.alternatizeUncurryFin_add, ContinuousLinearMap.isBigOTVS_fun_comp, SeparationQuotient.liftCLM_mk, ContinuousLinearMap.coeFn_compLp, ContinuousLinearMap.flip_zero, ContMDiffWithinAt.clm_prodMap, ContinuousAt.clm_comp, ContinuousLinearMap.isOpenMap, ContDiffMapSupportedIn.fderivCLM_apply, MeasureTheory.L1.setToL1_mono, TestFunction.fderivCLM_apply, fderivWithin_cosh, ContinuousMultilinearMap.norm_ofSubsingleton, ContinuousLinearMap.isAdjointPair_inner, VectorFourier.norm_fourierPowSMulRight_le, ContinuousLinearMap.coe_le_coe_iff, SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply, ContinuousLinearMap.coe_sub', ProbabilityTheory.norm_uncenteredCovarianceBilin_le, complexOfReal_hasDerivAt, Real.hasFDerivAt_fourierChar_neg_bilinear_right, ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, Unitization.splitMul_injective, ContinuousLinearMap.isUniformEmbedding_postcomp, ContDiffMapSupportedIn.continuous_iff_comp, ContinuousLinearMap.smulRight_comp, cfcₙ_eq_cfcₙL, DoubleCentralizer.sub_snd, ContDiffOn.comp_continuousLinearMap, VectorFourier.norm_fourierSMulRight, ContinuousLinearMap.smulRight_one_one, ContinuousLinearMap.nnnorm_id, fderivWithin_continuousAlternatingMap_apply, LinearEquiv.extend_apply, hom_chart, ContinuousLinearMap.isPositive_zero, ContinuousLinearMap.toUniformConvergenceCLM_continuous, hasStrictFDerivAt_inv', cfcₙL_apply, hasFDerivAt_exp_smul_const_of_mem_ball', SchwartzMap.smulLeftCLM_sub, Submodule.snd_orthogonalDecomposition_apply, TemperedDistribution.smulLeftCLM_const, hasFDerivAtFilter_natCast, SchwartzMap.smulLeftCLM_apply_apply, MDifferentiable.clm_apply, HasMFDerivAt.sum, SchwartzMap.fourier_fderivCLM_eq, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, ContinuousLinearMap.add_comp, ContinuousLinearMap.integral_comp_id_comm, hasStrictFDerivAt_exp_smul_const, SchwartzMap.fourier_convolution_apply, Complex.hasStrictFDerivAt_log_real, MeasureTheory.SimpleFunc.setToSimpleFunc_const', iteratedFDeriv_two_apply, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, LinearIsometry.norm_toContinuousLinearMap_le, Submodule.starProjection_le_starProjection_iff, TemperedDistribution.smulLeftCLM_sum, HasStrictFDerivAt.mul, ContinuousLinearMap.analyticOnNhd, ContMDiffAt.clm_apply, jacobiTheta₂_fderiv_undef, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2, hom_trivializationAt_apply, MDifferentiable.clm_precomp, ContinuousLinearMap.hasMFDerivWithinAt, ContinuousLinearEquiv.nnnorm_symm_pos, MDifferentiable.clm_comp, Real.differentiable_fourierChar_neg_bilinear_left, FormalMultilinearSeries.enorm_compContinuousLinearMap_le, ContDiffMapSupportedIn.fderivLM_apply_of_le, ContMDiff.clm_comp, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, continuousMultilinearCurryLeftEquiv_symm_apply, fderivWithin_add, ContinuousAffineMap.snd_decompLinearEquiv, LineDeriv.lineDerivOpCLM_apply, instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass, ContinuousMultilinearMap.smulRightL_apply, ContinuousLinearMap.contDiff, ContinuousLinearMap.instBorelSpace, Convex.second_derivative_within_at_symmetric_of_mem_interior, HasDerivAt.comp_hasFDerivAt, fderiv_mul_const, ContinuousLinearMap.isUniformEmbedding_toUniformOnFun, fderiv_csinh, ContinuousLinearMap.exists_mul_lt_of_lt_opNorm, toWeakSpaceCLM_eq_toWeakSpace, HasStrictFDerivAt.fun_add, IsLocalMinOn.fderivWithin_nonneg, Complex.reCLM_norm, ContinuousLinearMap.norm_snd_le, Submodule.orthogonalDecomposition_apply, iteratedFDeriv_succ_eq_comp_left, fderiv_of_notMem_tsupport, ContinuousLinearMap.smul_compLpL, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, hasStrictFDerivAt_const, ContinuousLinearMap.contMDiffOn, VonNeumannAlgebra.instStarMemClass, CovariantDerivative.torsion_apply_eq_extend, ContDiffMapSupportedIn.fderivLM_apply_of_gt, EuclideanSpace.restrict₂_apply, Convex.norm_image_sub_le_of_norm_fderiv_le', contMDiffOn_coordChangeL, ContinuousLinearEquiv.arrowCongrSL_symm_apply, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ, ContinuousLinearMap.nnbound, ContinuousLinearMap.opNorm_mulLeftRight_le, DoubleCentralizer.intCast_fst, PointwiseConvergenceCLM.evalCLM_apply, topDualPairing_apply, isCompactOperator_of_locallyCompactSpace_dom, ContinuousLinearMap.norm_compLpL_le, ContinuousLinearMap.comp_sub, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left, ContDiffMapSupportedIn.structureMapCLM_zero_injective, Module.Basis.opNNNorm_le, MeasureTheory.setIntegral_condExpL1CLM, ContMDiffWithinAt.clm_precomp, ContinuousMultilinearMap.ofSubsingletonₗᵢ_apply, IsLocalMin.fderiv_eq_zero, norm_iteratedFDerivWithin_fderivWithin, ContinuousLinearMap.cpolynomialOn, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, ContinuousLinearMap.coe_complexOfReal, LinearMap.coe_toContinuousLinearMap_symm, HasFDerivWithinAt.finset_prod, hasStrictFDerivAt_list_prod', ContinuousLinearMap.le_opENorm, continuousMultilinearCurryFin1_symm_apply, MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound, ContinuousLinearMap.coe_mul, hom_trivializationAt_baseSet, Submodule.orthogonal_eq_inter, ContinuousLinearMap.mdifferentiableOn, MeasureTheory.eLpNorm_condExpL2_le, Complex.integral_boundary_rect_of_differentiableOn_real, ContinuousLinearMap.lsmul_flip_apply, SchwartzMap.coe_apply, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, SchwartzMap.smulLeftCLM_ofReal, extDerivWithin_apply, ContinuousAt.clm_bundle_apply, fderivWithin_zero_of_not_differentiableWithinAt, ContinuousLinearMap.prodₗ_apply, ContinuousLinearMap.sSup_unitClosedBall_eq_norm, ContinuousLinearMap.coprodEquiv_symm_apply, iteratedDeriv_vcomp_two, fderiv_norm_rpow, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, MeasureTheory.L1.integral_eq', ContDiffOn.smulRight, ContinuousLinearMap.opNorm_eq_of_bounds, Submodule.starProjection_orthogonal_val, VectorField.lieBracketWithin_eq, ContinuousLinearMap.coe_injective, ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap, isStarProjection_iff_eq_starProjection, ContinuousAlternatingMap.liftCLM_apply, ContinuousLinearMap.norm_adjoint_comp_self, ContinuousLinearEquiv.coe_coe, SchauderBasis.RankOneDecomposition.proj_comp, ContinuousLinearMap.map_add₂, ContinuousAffineMap.snd_decompAffineEquiv, MeasureTheory.integral_bilinear_hasDerivAt_eq_sub, ContMDiff.clm_precomp, VonNeumannAlgebra.instSubringClass, VectorField.fderivWithin_apply_lieBracket, ContinuousAffineMap.vsub_contLinear, fderivWithin_pow, ContinuousLinearMap.continuousConstSMul_apply, HasFPowerSeriesWithinAt.compContinuousLinearMap, VectorPrebundle.coordChange_apply, ContinuousLinearMap.isCentralScalar, EuclideanGeometry.orthogonalProjection_apply, hasFDerivAt_exp_zero_of_radius_pos, fderivWithin_fun_const_smul, Bundle.ContinuousLinearMap.memTrivializationAtlas, ContMDiffOn.clm_prodMap, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono, ContinuousLinearMap.hasDerivWithinAt, hasStrictFDerivAt_pow, FormalMultilinearSeries.derivSeries_apply_diag, ContMDiffWithinAt.clm_comp, Submodule.norm_orthogonalProjection, AnalyticAt.fderiv, fderiv_comp_smul, iteratedFDeriv_clm_apply_const_apply, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, ContinuousLinearMap.opNorm_lsmul, ProbabilityTheory.covarianceBilinDual_of_not_memLp, fderivWithin_arctan, TemperedDistribution.smulLeftCLM_smul, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn, curveIntegral_add, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv, ContinuousLinearMap.prod_apply, Complex.imCLM_apply, integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable, InnerProductSpace.continuousLinearMapOfBilin_apply, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NormedSpace.double_dual_bound, Matrix.cstar_norm_def, MeasureTheory.convolution_eq_swap, ContinuousLinearMap.map_zero₂, Module.Basis.opNorm_le, fderivWithin_def, UniformCauchySeqOnFilter.one_smulRight, Real.zero_at_infty_vector_fourierIntegral, ContDiff.fderiv_right, VectorField.mlieBracketWithin_apply, SchwartzMap.smulLeftCLM_apply, ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, fderiv_csin, ContinuousLinearMap.norm_snd, MeasureTheory.condExpIndSMul_ae_eq_smul, ContinuousLinearMap.iteratedFDeriv_comp_right, norm_fderiv_le_of_lip', ContinuousLinearMap.rayleighQuotient_neg_apply, HasFDerivAtFilter.isEquivalent_sub, fderiv_cosh, ContinuousAffineMap.decompAffineEquiv_symm_contLinear, support_fderiv_subset, HasStrictFDerivAt.fun_mul, ContDiff.continuousLinearMap_comp, ContinuousLinearMap.precomp_apply, ContinuousLinearMap.norm_holderL_le, hasFDerivWithinAt_pow, contDiff_infty_iff_fderiv, hasFDerivWithinAt_iff_isLittleOTVS, ContinuousAffineMap.toConstProdContinuousLinearMap_fst, curveIntegral_sub, cfcₙL_integrable, HasFDerivWithinAt.mul', HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn, HasGradientAt.fderiv_apply, differentiableWithinAt_complex_iff_differentiableWithinAt_real, ContinuousLinearMap.comp_analyticOnNhd, TemperedDistribution.derivCLM_apply_apply, MeasureTheory.L1.setToL1'_eq_setToL1SCLM, ContinuousAlternatingMap.norm_compContinuousLinearMap_le, ContinuousLinearMap.locallyIntegrableOn_comp, ContinuousLinearMap.precomp_uniformConvergenceCLM_apply, mfderiv_subtype_coe_Icc_one, ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm, Polynomial.hasFDerivWithinAt, Real.hasStrictFDerivAt_rpow_of_neg, ContinuousLinearMap.coe_pi', IsCovariantDerivativeOn.affine_combination, ContinuousLinearMap.postcompUniformConvergenceCLM_apply, MeasureTheory.weightedSMul_smul_measure, VectorField.lieBracket_smul_right, ContinuousLinearMap.coeFn_ofSeqClosedGraph, intervalIntegral.integral_hasFDerivAt, CurveIntegrable.sub, InnerProductSpace.HarmonicAt.comp_CLM, HasFiniteFPowerSeriesOnBall.fderiv_eq, ContinuousLinearMap.isHomeomorph_of_isUnit, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound, TestFunction.lineDerivCLM_apply_of_gt, ContinuousLinearMap.smulRight_apply, HasStrictDerivAt.complexToReal_fderiv, intervalIntegral.fderiv_integral, PiTensorProduct.mapL_add, fderiv_fun_const, ContinuousLinearMap.analyticAt_bilinear, inner_gradient_left, FormalMultilinearSeries.compContinuousLinearMap_apply, eventually_norm_trivializationAt_lt, ConvexOn.exists_affine_le_of_lt, ProbabilityTheory.IsGaussian.charFunDual_eq', HasFDerivWithinAt.comp_hasDerivAt_of_eq, HasFPowerSeriesAt.hasStrictFDerivAt, contDiffOn_fderivWithin_apply, ContinuousLinearMap.toPointwiseConvergenceCLM_apply, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, ContinuousLinearMap.pi_zero, IsCovariantDerivativeOn.torsion_apply, innerSL_apply_coe, ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp, fderivWithin_mul', ContinuousLinearMap.bound, MeasureTheory.eLpNorm_le_eLpNorm_fderiv, HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq, ContinuousLinearMap.isPositive_one, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, ContinuousLinearMap.isPositive_sum, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite, MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg, ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, MeasureTheory.ContinuousMap.inner_toLp, Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff, ConvexOn.real_sSup_of_nat_affine_eq, integral_bilinear_fderiv_right_eq_neg_left_of_integrable, hasFDerivAt_inv', MeasureTheory.dominatedFinMeasAdditive_weightedSMul, ContinuousLinearMap.coe_mk', DifferentiableAt.comp_semilinear₂, exists_continuousLinearEquiv_fderiv_symm_eq, TensorialAt.mkHom₂_apply_eq_extend, MeasureTheory.AEStronglyMeasurable.convolution_integrand', mfderiv_neg, ContinuousLinearMap.map_neg, hasFDerivWithinAt_of_subsingleton, ContinuousLinearMap.IsInvertible.self_apply_inverse, ContinuousLinearMap.isPositive_adjoint_comp_self, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, ContinuousLinearMap.integral_comp_comm, hasFDerivWithinAt_iff_tendsto, ContinuousLinearMap.map_neg₂, Matrix.l2_opNorm_def, ContinuousLinearMap.coe_toContinuousAffineMap, ContinuousMultilinearMap.norm_compContinuousLinearMapL_le, Bundle.RiemannianMetric.continuousAt, ContinuousLinearMap.iteratedFDeriv_comp_left, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed, Submodule.orthogonalProjection_eq_zero_iff, ContinuousLinearMap.holderL_apply_apply, HasFDerivAt.isEquivalent_sub, Complex.reCLM_enorm, MeasureTheory.condExpInd_empty, ContMDiffOn.clm_bundle_apply, MeasureTheory.condExpL1CLM_smul, isConformalMap_const_smul, MeasureTheory.AEStronglyMeasurable.convolution_integrand, Complex.norm_fderiv_le_div_of_mapsTo_ball, norm_innerSL_le, VectorFourier.hasFDerivAt_fourierChar_smul, HasStrictFDerivAt.sub, ContMDiffWithinAt.cle_arrowCongr, ContinuousLinearMap.isLeast_opNorm, ContinuousLinearMap.IsInvertible.injective, ContinuousLinearMap.comp_fst_add_comp_snd, fderiv_const_smul_of_field, ContinuousLinearMap.IsPositive.isSelfAdjoint, Submodule.orthogonalProjection_starProjection_of_le, GeneralSchauderBasis.proj_comp, continuousMultilinearCurryRightEquiv_apply, hasStrictFDerivAt_intCast, ContinuousLinearMap.integrableOn_comp, Submodule.coe_orthogonalProjection_apply, ContinuousLinearMap.integrable_of_bilin_of_bdd_right, HasFDerivAt.neg, ContinuousLinearMap.intrinsicStar_apply, SeparationQuotient.mkCLM_apply, ContinuousLinearMap.coe_smul, fderiv_comp_deriv_of_eq, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply, ContinuousLinearMap.extend_eq, ContinuousLinearMap.apply_apply', HasFPowerSeriesWithinAt.hasFDerivWithinAt, ProbabilityTheory.covarianceBilinDual_of_not_memLp', UnconditionalSchauderBasis.exists_norm_proj_le, ContDiff.fderiv, Submodule.starProjection_apply_eq_zero_iff, fderiv_list_prod', SchwartzMap.fourier_convolution, HasMFDerivWithinAt.prod, AnalyticOnNhd.eval_continuousLinearMap', fderivWithin_comp_smul, ContinuousLinearMap.apply_val_ker, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, HasMFDerivAt.mul', ContinuousLinearMap.flipₗᵢ_symm, HasFPowerSeriesAt.compContinuousLinearMap, ImplicitFunctionData.rightDeriv_fderiv_implicitFunction, fderivWithin_clm_apply, TopModuleCat.hom_neg, ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply, exists_continuousLinearEquiv_fderivWithin_symm_eq, ContinuousLinearMap.instLocallyBoundedMapClass, ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz, ContinuousLinearMap.coe_one, AlternatingMap.mkContinuousLinear_norm_le_max, ContinuousLinearMap.dist_le_opNorm, FormalMultilinearSeries.rightInv_coeff_one, FourierTransform.fourierCLM_apply, ContinuousAffineMap.zero_contLinear, hasFDerivAt_exp, fderiv_continuousAlternatingMap_apply_const_apply, InnerProductGeometry.IsConformalMap.preserves_angle, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, complexOfReal_derivWithin, ApproximatesLinearOn.lipschitzOnWith, norm_fderiv_norm_id_rpow, ContinuousLinearMap.isBigOTVS_id, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure, ContinuousLinearMap.norm_holder_apply_apply_le, ClosedSubmodule.coe_comap, ContinuousLinearMap.homothety_norm, fderivWithin_sum, RKHS.posSemidef_kernel, Submodule.norm_subtypeL_le, ContinuousLinearMap.hasStrictDerivAt, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, fderivWithin_pow_ring, fderiv_const_smul, ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap, measurable_fderiv_apply_const_with_param, ContinuousLinearEquiv.fst_equivOfRightInverse, ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, ContinuousLinearMap.bound_of_antilipschitz, HasStrictFDerivAt.clm_comp, WithLp.fstL_apply, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, DoubleCentralizer.toProdHom_apply, DoubleCentralizer.mul_snd, VectorFourier.fourierIntegral_fderiv, ContinuousLinearMap.fpowerSeries_apply_one, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, MeasureTheory.L1.integral_eq, fderiv_continuousLinearEquiv_comp', ContinuousLinearMap.smulRightL_apply_apply, continuousOn_clm_apply, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, ContinuousLinearMap.toSpanSingletonCLE_apply_apply, MDifferentiableWithinAt.clm_prodMap, HasFDerivAt.fun_mul', ContMDiffAt.clm_comp, HasStrictFDerivAt.continuousMultilinearMap_apply, MeasureTheory.weightedSMul_zero_measure, HasStrictFDerivAt.mul_const, ContinuousAlternatingMap.compContinuousLinearMapCLM_apply, ContinuousMultilinearMap.norm_compContinuousLinearMap_le, ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left, ContinuousLinearMap.opNNNorm_mul_apply, fderivInnerCLM_apply, eventually_norm_mfderiv_extChartAt_lt, ContDiffAt.smulRight, TestFunction.injective_toBoundedContinuousFunctionCLM, ConvexOn.sSup_affine_eq, VectorBundleCore.coordChange_comp, MeasureTheory.L1.setToL1'_apply_coeToLp, SchwartzMap.denseRange_toLpCLM, SchwartzMap.toZeroAtInftyCLM_apply, ContinuousLinearMap.toSpanSingletonCLE_symm_apply, mdifferentiableWithinAt_hom_bundle, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, ContinuousLinearMap.norm_precompL_le, Real.fderiv_fourierChar_neg_bilinear_left_apply, isConformalMap_iff_is_complex_or_conj_linear, ContinuousLinearMap.apply_apply, MeasureTheory.L1.setToL1_const, ContinuousLinearMap.norm_map_removeNth_le, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply, IsSymmSndFDerivWithinAt.eq, ContinuousLinearMap.map_smulₛₗ₂, CurveIntegrable.add, PiTensorProduct.mapLMultilinear_opNorm, fderivWithin_restrictScalars_comp, hasFDerivAt_tsum_of_isPreconnected, LinearMap.canLiftContinuousLinearMap, ContinuousLinearMap.instModuleFinite, fderivWithin_fun_sum, ContinuousOn.clm_bundle_apply, inner_gradient_right, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, Real.fourierIntegral_iteratedFDeriv, Submodule.orthogonalProjection_norm_le, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, HasFDerivAt.mul', DoubleCentralizer.intCast_toProd, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, derivWithin_clm_apply, fderiv_single, hom_trivializationAt_target, SchwartzMap.fourierMultiplierCLM_smul, Submodule.orthogonalProjection_orthogonal, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, hasFDerivAt_list_prod_attach', MeasureTheory.L1.setToL1_lipschitz, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd, TemperedDistribution.fourierTransformInvCLM_apply, MeasureTheory.norm_condExpL2_le_one, MDifferentiableWithinAt.clm_apply, HasCompactSupport.convolution_integrand_bound_right, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, fderivWithin_mem_iff, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, MeasureTheory.setToFun_eq, DifferentiableAt.lineDeriv_eq_fderiv, HasDerivAt.comp_semilinear, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply, MeasureTheory.condExpL2_comp_continuousLinearMap, ConvexOn.real_sSup_affine_eq, InnerProductSpace.symm_toEuclideanLin_rankOne, isBoundedBilinearMap_smulRight, ContinuousOn.continuousLinearMapCoprod, ContMDiffAt.cle_arrowCongr, AnalyticOnNhd.eval_continuousLinearMap, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, HasDerivWithinAt.comp_hasFDerivAt_of_eq, HasFDerivAt.clm_comp, ContinuousLinearMap.adjoint_innerSL_apply, hasFDerivAt_iff_isLittleO_nhds_zero, ContinuousLinearMap.isQuotientMap, Bundle.Pretrivialization.continuousLinearMapCoordChange_apply, ContinuousLinearMap.circleAverage_comp_comm, fderiv_tsum_apply, ContinuousLinearMap.mem_invtSubmodule_adjoint_iff, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, ContinuousLinearMap.coprodEquivL_symm_apply, VectorPrebundle.contMDiffCoordChange_apply, fderivWithin_fun_mul, ContinuousLinearMap.isUniformEmbedding_of_bound, ContinuousOn.prod_map_equivL, Submodule.orthogonalProjection_eq_linearProjOfIsCompl, continuousOn_coordChange, HasCompactSupport.convolution_integrand_bound_right_of_subset, ContinuousLinearMap.IsPositive.re_inner_nonneg_right, DoubleCentralizer.smul_snd, postcomp_compactConvergenceCLM_apply, ContinuousLinearMap.integral_id_map, ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff, second_derivative_symmetric_of_eventually_of_real, BoundedContinuousFunction.toLp_denseRange, MeasureTheory.condExpL2_const_inner, ContinuousLinearMap.HasRightInverse.surjective, TemperedDistribution.laplacianCLM_apply, ContinuousLinearMap.toWOT_apply, contMDiffWithinAt_hom_bundle, ContinuousLinearMap.one_def, mem_contMDiffFiberwiseLinear_iff, ContinuousLinearMap.zero_smulRight, curveIntegralFun_def, ContinuousLinearMap.ext_ring_iff, ContinuousLinearMap.norm_smulRightL_apply, ContinuousAlternatingMap.alternatizeUncurryFin_apply, ContinuousLinearMap.intervalIntegral_comp_comm, HasFDerivAt.smul, ContinuousLinearMap.contMDiffAt, isOpen_setOf_nat_le_rank, ContinuousLinearMap.zero_apply, SchwartzMap.smulLeftCLM_smul, CurveIntegrable.neg, isClosed_setOf_isCompactOperator, SchauderBasis.sum_succSub, DoubleCentralizer.coe_snd, ContinuousLinearMap.opNorm_le_bound₂, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, MeasureTheory.integral_convolution, ContinuousLinearMap.le_opNorm_enorm, fderiv_norm_sq_apply, Submodule.starProjection_eq_self_iff, fderiv_sin, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, ContinuousMultilinearMap.norm_curryMid, ConvexOn.univ_sSup_of_nat_affine_eq, InnerProductGeometry.ConformalAt.preserves_angle, Submodule.starProjection_tendsto_closure_iSup, hasFDerivAt_exp_of_mem_ball, norm_iteratedFDeriv_fderiv, MeasureTheory.Lp.toTemperedDistribution_smul_eq, NormedSpace.dual_def, SchwartzMap.laplacian_eq_fourierMultiplierCLM, HasFDerivAtFilter.hasDerivAtFilter, HasFDerivAt.isLittleOTVS, ContinuousAlternatingMap.ofSubsingleton_symm_apply_apply, const_smul_mfderiv, fderiv_norm_sq, ContinuousLinearMap.opNorm_le_of_lipschitz, HasMFDerivAt.const_smul, IsCovariantDerivativeOn.finite_affine_combination, ContinuousLinearMap.coe_mulₗᵢ, ContinuousLinearMap.isUnit_iff_bijective, MDifferentiableOn.clm_bundle_apply₂, MeasureTheory.condExpL1_eq, OrthogonalFamily.projection_directSum_coeAddHom, HasFDerivWithinAt.continuousAlternatingMap_apply_const, ContinuousLinearMap.innerSL_apply_comp, ApproximatesLinearOn.to_inv, TopModuleCat.hom_forget₂_TopCat_map, conformalAt_iff', ContinuousLinearMap.instStarOrderedRingRCLike, ContinuousLinearMap.mdifferentiableAt, ContinuousLinearMap.toSesqForm_apply_norm_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd, PiTensorProduct.injectiveSeminorm_def, ContinuousLinearMap.coeFn_holder, MeasureTheory.L1.SimpleFunc.setToL1S_smul_left, ContinuousLinearMap.map_smul, CStarMatrix.norm_def, ContMDiff.cle_arrowCongr, ContinuousLinearMap.coe_deriv₂, IsMIntegralCurveAt.eventually_hasDerivAt, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, ContMDiffOn.clm_bundle_apply₂, contDiff_succ_iff_hasFDerivAt, MeasureTheory.Measure.ContinuousLinearMap.quasiMeasurePreserving, ContinuousWithinAt.clm_bundle_apply, extDeriv_apply, mfderiv_prod_eq_add_apply, MeasureTheory.condExpL2_indicator_nonneg, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply, ContinuousLinearMap.adjoint_adjoint, HasCompactSupport.hasFDerivAt_convolution_left, fderivWithin_mul, DoubleCentralizer.add_toProd, Continuous.prod_mapL, Bundle.ContinuousRiemannianMetric.isVonNBounded, ContinuousLinearMap.comp_toSpanSingleton, HasStrictDerivAt.clm_apply, HasFDerivWithinAt.sum, TemperedDistribution.smulLeftCLM_apply_apply, HasFDerivWithinAt.isLittleO, ContinuousLinearMap.closure_preimage, MeasureTheory.SimpleFunc.map_setToSimpleFunc, ContinuousLinearMap.is_weak_closed_closedBall, ContinuousLinearMap.opNorm_le_of_re_inner_le, fderiv_inner_apply, ContinuousLinearMap.hasDerivAt_of_bilinear, ProbabilityTheory.covarianceOperator_of_not_memLp, second_derivative_symmetric_of_eventually, HasFDerivAt.comp_hasDerivAt_of_eq, ContMDiff.coordChangeL, SeparationQuotient.outCLM_injective, fderiv_const_apply, ContinuousMultilinearMap.norm_ofSubsingleton_id, HasFDerivWithinAt.fun_mul, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left', NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, HasStrictFDerivAt.smul, ContinuousLinearMap.orthogonal_ker, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, ContinuousLinearMap.HasLeftInverse.injective, ContDiffWithinAt.fderivWithin_right, ContinuousLinearMap.LinearMap.IsSymmetricProjection.isStarProjection, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, HasStrictFDerivAt.finset_prod, contDiffWithinAt_succ_iff_hasFDerivWithinAt, Asymptotics.IsBigO.hasFDerivAt, InnerProductSpace.norm_rankOne, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, HasFDerivAt.fun_sub, hasFDerivAt_integral_of_dominated_loc_of_lip, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero, DoubleCentralizer.neg_fst, PiTensorProduct.mapLMultilinear_toFun_apply, VectorField.mlieBracket_smul_right, CStarMatrix.inner_toCLM_conjTranspose_right, norm_jacobiTheta₂_term_fderiv_le, HasFiniteFPowerSeriesOnBall.fderiv, ContinuousLinearEquiv.norm_pos, iteratedDerivWithin_vcomp_three, ContinuousAffineMap.toConstProdContinuousLinearMap_snd, ContinuousLinearMap.antilipschitz_of_forall_le_inner_map, MDifferentiableAt.clm_apply, HasFDerivAt.isLittleO, ContinuousMultilinearMap.curryMidEquiv_symm_apply, fderiv_eq_smul_deriv, unitary.inner_map_map, CStarMatrix.toCLM_apply_single_apply, HasMFDerivWithinAt.mfderivWithin_eq_zero, ContinuousMultilinearMap.uncurryRight_norm, ContinuousLinearMap.flipAlternating_apply_apply, LinearMap.ker_toContinuousLinearMap, ContinuousLinearMap.comp_smul, hasStrictFDerivAt_exp_smul_const_of_mem_ball, DoubleCentralizer.toProdMulOppositeHom_apply, ContinuousLinearMap.coeFn_compLp', ContinuousLinearMap.coe_zero, MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap, ContinuousLinearMap.algebraMap_apply, ContinuousLinearMap.comp_apply, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable, curveIntegralFun_zero, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, hasFDerivAtFilter_intCast, ContinuousLinearMap.coe_completion, iteratedFDeriv_succ_apply_left, ContDiffWithinAt.fderivWithin_apply, IsSymmSndFDerivAt.eq, hasFDerivAtFilter_one, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux, Complex.restrictScalars_toSpanSingleton', HasFDerivWithinAt.list_prod', HasFDerivAt.continuousMultilinearMap_apply, ContinuousLinearMap.finset_sum_comp, fderiv_inv', SeparationQuotient.outCLM_isUniformInducing, ContinuousLinearMap.coeFn_ofIsClosedGraph, Continuous.fderiv_one, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, IsLocalMinOn.fderivWithin_eq_zero, Submodule.mem_iff_norm_starProjection, Complex.reCLM_apply, fderivWithin_pow', ContinuousLinearEquiv.ofBijective_apply_symm_apply, continuousMultilinearCurryFin1_apply, IsCoercive.antilipschitz, LinearMap.IsSymmetric.apply_clm, hasFDerivAt_finset_prod, unitary.linearIsometryEquiv_coe_apply, ContinuousLinearMap.IsInvertible.inverse_apply_eq, norm_iteratedFDeriv_clm_apply_const, LinearIsometry.adjoint_comp_self

---

← Back to Index