LinearMap

📁 Source: Mathlib/Topology/Algebra/Module/LinearMap.lean

Statistics

Metric	Count
Definitions apply, add, addCommGroup, addCommMonoid, algebra, applyModule, codRestrict, coeLM, coeLMₛₗ, comp, copy, distribMulAction, funLike, homeomorphOfUnit, id, inhabited, instMul, instNatCast, instSMul, monoidWithZero, mulAction, neg, one, projKerOfRightInverse, rangeRestrict, restrictScalars, restrictScalarsₗ, semiring, smulRight, smulRightₗ, sub, toLinearMap, toLinearMapRingHom, toSpanSingleton, toSpanSingletonLE, uniqueOfLeft, uniqueOfRight, zero, «term_∘L_», ContinuousLinearMapClass, ContinuousSemilinearMapClass, StrongDual, ClosedComplemented, complement, subtypeL, topDualPairing, «term_→L[_]_», «term_→SL[_]_»	48
Theorems commute_iff, commute_iff_of_isUnit, conj_eq_of_ker_mem_invtSubmodule, conj_eq_of_range_mem_invtSubmodule, ext, ext_iff, isClosed_range, ker_eq_range, ker_mem_invtSubmodule, ker_mem_invtSubmodule_iff, range_eq_ker, range_mem_invtSubmodule, range_mem_invtSubmodule_iff, toLinearMap, add_apply, add_comp, algebraMap_apply, applyFaithfulSMul, applySMulCommClass, applySMulCommClass', apply_val_ker, cancel_left, closedComplemented_ker_of_rightInverse, coeFn_injective, coeLM_apply, coeLMₛₗ_apply, coe_add, coe_add', coe_codRestrict, coe_codRestrict_apply, coe_coe, coe_comp, coe_comp', coe_copy, coe_eq_id, coe_id, coe_id', coe_inj, coe_injective, coe_mk, coe_mk', coe_mul, coe_mul', coe_neg, coe_neg', coe_one, coe_pow, coe_pow', coe_projKerOfRightInverse_apply, coe_rangeRestrict, coe_restrictScalars, coe_restrictScalars', coe_restrictScalarsₗ, coe_smul, coe_smul', coe_smulRight, coe_smulRightₗ, coe_sub, coe_sub', coe_sum, coe_sum', coe_zero, coe_zero', comp_add, comp_apply, comp_assoc, comp_finset_sum, comp_id, comp_neg, comp_smul, comp_smulₛₗ, comp_sub, comp_toSpanSingleton, comp_zero, completeSpace_eqLocus, completeSpace_ker, cont, continuous, continuousConstSMul_apply, continuousSemilinearMapClass, continuous_toLinearMap, copy_eq, default_def, eqOn_closure_span, exists_ne_zero, ext, ext_iff, ext_on, ext_ring, ext_ring_iff, finset_sum_comp, homeomorphOfUnit_apply, homeomorphOfUnit_symm_apply, id_apply, id_comp, instNontrivialId, intCast_apply, isCentralScalar, isClosed_ker, isComplete_ker, isHomeomorph_of_isUnit, isIdempotentElem_toLinearMap_iff, isOpenMap_of_ne_zero, isScalarTower, ker_codRestrict, leftInverse_of_comp, map_add, map_neg, map_smul, map_smul_of_tower, map_smulₛₗ, map_sub, map_zero, mul_apply, mul_def, natCast_apply, neg_apply, neg_comp, ofNat_apply, one_apply, one_def, one_smulRight_eq_toSpanSingleton, projKerOfRightInverse_apply_idem, projKerOfRightInverse_comp_inv, range_coeFn_eq, range_smulRight_apply, range_toLinearMap, restrictScalars_add, restrictScalars_neg, restrictScalars_smul, restrictScalars_sub, restrictScalars_zero, rightInverse_of_comp, smulCommClass, smulRight_apply, smulRight_comp, smulRight_comp_smulRight, smulRight_id, smulRight_one_eq_iff, smulRight_one_eq_toSpanSingleton, smulRight_one_one, smulRight_one_pow, smulRight_zero, smul_apply, smul_comp, smul_def, sub_apply, sub_apply', sub_comp, sum_apply, toContinuousAddMonoidHom_add, toContinuousAddMonoidHom_comp, toContinuousAddMonoidHom_id, toContinuousAddMonoidHom_inj, toContinuousAddMonoidHom_injective, toContinuousAddMonoidHom_neg, toContinuousAddMonoidHom_restrictScalars, toContinuousAddMonoidHom_sub, toContinuousAddMonoidHom_zero, toLinearMapRingHom_apply, toLinearMap_toSpanSingleton, toSpanSingletonLE_apply, toSpanSingletonLE_symm_apply, toSpanSingleton_add, toSpanSingleton_apply, toSpanSingleton_apply_map_one, toSpanSingleton_apply_one, toSpanSingleton_comp, toSpanSingleton_comp_toSpanSingleton, toSpanSingleton_inj, toSpanSingleton_one, toSpanSingleton_pow, toSpanSingleton_smul, toSpanSingleton_zero, uniformContinuous, zero_apply, zero_comp, zero_smulRight, toContinuousMapClass, toSemilinearMapClass, topologicalClosure_map_submodule, exists_isClosed_isCompl, isClosed, isClosed_complement, isCompl_complement, closedComplemented_bot, closedComplemented_top, coe_subtypeL, coe_subtypeL', ker_subtypeL, range_subtypeL, subtypeL_apply, topologicalClosure_map, topologicalClosure_mem_invtSubmodule, topDualPairing_apply	195
Total	243

ContinuousLinearMap

Definitions

Name	Category	Theorems
add 📖	CompOp	182 math math: Matrix.l2_opNorm_toEuclideanCLM, mfderiv_prod_eq_add, coe_add, MeasureTheory.setToFun_add_left, HasDerivWithinAt.clm_comp, HasStrictFDerivAt.fun_mul', HasMFDerivAt.mul, HasFDerivWithinAt.continuousMultilinearMap_apply, Complex.restrictScalars_one_smulRight', HasMFDerivAt.add, fderivWithin_fun_smul, HasFDerivWithinAt.add, Matrix.cstar_nnnorm_def, HasDerivWithinAt.complexToReal_fderiv', toContinuousAddMonoidHom_add, ContMDiffCovariantDerivativeOn.affine_combination, HasFDerivWithinAt.clm_apply, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, Unitization.splitMul_apply, HasFDerivAt.fun_mul, fderiv_clm_comp, HasStrictFDerivAt.mul', HasFDerivWithinAt.linear_multilinear_comp, fderiv_fun_smul, LinearIsometryEquiv.conjStarAlgEquiv_apply, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, Real.hasStrictFDerivAt_rpow_of_pos, HasFDerivWithinAt.continuousAlternatingMap_apply, HasStrictDerivAt.clm_comp, derivWithin_clm_comp, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivWithinAt.mul, hasFDerivWithinAt_of_bilinear, HasFDerivAt.fun_smul, fderiv_continuousAlternatingMapCompContinuousLinearMap, MeasureTheory.L1.SimpleFunc.setToL1S_add_left, comp_add, hasStrictFDerivAt_of_bilinear, Complex.hasStrictFDerivAt_cpow', HasMFDerivAt.smul, HasFDerivAt.add, fderiv_continuousAlternatingMap_apply, HasFDerivAt.clm_apply, HasFDerivAt.continuousAlternatingMap_apply, fderiv_smul, MeasureTheory.SimpleFunc.setToSimpleFunc_add_left, mfderiv_prod_eq_add_comp, fderiv_of_bilinear, HasFDerivWithinAt.fun_smul, Matrix.toEuclideanCLM_toLp, Complex.hasStrictFDerivAt_cpow, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, HasFDerivWithinAt.cpow, fderivWithin_of_bilinear, DoubleCentralizer.add_fst, fderiv_mul, coprod_add, MeasureTheory.condExpInd_disjoint_union, TopModuleCat.hom_add, fderiv_fun_add, LinearIsometryEquiv.conjStarAlgEquiv_trans, HasStrictFDerivAt.rpow, fderivWithin_fun_mul', add_apply, fderiv_mul', LinearIsometryEquiv.conjStarAlgEquiv_refl, HasDerivAt.complexToReal_fderiv', CovariantDerivative.affine_combination_toFun, restrictScalars_add, fromTangentSpace_mfderiv_smul', HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, Complex.hasFDerivAt_cpow, Matrix.inner_toEuclideanCLM, TestFunction.lineDerivCLM_add, DoubleCentralizer.add_snd, rayleighQuotient_add, fderivWithin_smul, mfderiv_add, IsCovariantDerivativeOn.leibniz, HasDerivAt.clm_comp, HasStrictFDerivAt.add, Unitization.norm_eq_sup, Matrix.ofLp_toEuclideanCLM, coe_add', MeasureTheory.weightedSMul_add_measure, curveIntegral_fun_add, extDerivFun_add, opNorm_add_le, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, flip_add, SchwartzMap.smulLeftCLM_add, HasMFDerivWithinAt.mul', HasFDerivAtFilter.fun_add, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, HasStrictFDerivAt.continuousAlternatingMap_apply, ContinuousAffineMap.add_contLinear, HasStrictDerivAt.complexToReal_fderiv', HasFDerivAt.mul, MeasureTheory.weightedSMul_union, fderiv_add, IsPositive.add, TemperedDistribution.smulLeftCLM_add, fderiv_fun_mul', HasFDerivAtFilter.add, HasFDerivWithinAt.clm_comp, fromTangentSpace_mfderiv_smul, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, IsCovariantDerivativeOn.add, HasMFDerivWithinAt.add, curveIntegralFun_add, deriv_clm_comp, fderivWithin_fun_add, MeasureTheory.weightedSMul_union', IsCovariantDerivativeOn.add_one_form, fderiv_continuousMultilinearMapCompContinuousLinearMap, LinearIsometryEquiv.symm_conjStarAlgEquiv, HasFDerivAt.fun_add, toSpanSingleton_add, ContinuousAffineMap.vadd_contLinear, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, fderivWithin_clm_comp, HasFDerivWithinAt.rpow, hasFDerivAt_uncurry_of_multilinear, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, Unitization.nnnorm_eq_sup, Matrix.toLin_finTwoProd_toContinuousLinearMap, add_compLp, HasMFDerivWithinAt.mul, HasStrictFDerivAt.clm_apply, HasStrictFDerivAt.fun_smul, HasStrictFDerivAt.cpow, fderiv_fun_mul, hasFDerivAt_of_bilinear, Submodule.id_eq_sum_starProjection_self_orthogonalComplement, ContinuousAlternatingMap.curryLeft_add, HasFDerivWithinAt.smul, fderiv_clm_apply, HasFDerivWithinAt.fun_mul', hasStrictFDerivAt_list_prod, add_compLpL, HasFDerivWithinAt.fun_add, mfderiv_smul, ContinuousAlternatingMap.alternatizeUncurryFin_add, fderivWithin_continuousAlternatingMap_apply, add_comp, HasStrictFDerivAt.mul, fderivWithin_add, HasStrictFDerivAt.fun_add, curveIntegral_add, Matrix.cstar_norm_def, HasStrictFDerivAt.fun_mul, HasFDerivWithinAt.mul', HasFDerivAt.cpow, Real.hasStrictFDerivAt_rpow_of_neg, IsCovariantDerivativeOn.affine_combination, PiTensorProduct.mapL_add, fderivWithin_mul', HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, comp_fst_add_comp_snd, HasMFDerivAt.mul', fderivWithin_clm_apply, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasStrictFDerivAt.clm_comp, HasFDerivAt.fun_mul', HasStrictFDerivAt.continuousMultilinearMap_apply, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, CurveIntegrable.add, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, HasFDerivAt.mul', HasFDerivAt.clm_comp, HasFDerivAt.rpow, fderivWithin_fun_mul, HasFDerivAt.smul, fderivWithin_mul, DoubleCentralizer.add_toProd, HasFDerivWithinAt.fun_mul, HasStrictFDerivAt.smul, Complex.restrictScalars_toSpanSingleton', HasFDerivAt.continuousMultilinearMap_apply
addCommGroup 📖	CompOp	190 math math: HasDerivWithinAt.clm_comp, topDualPairing_isContPerfPair, isPositive_iff_eq_sum_rankOne, Bundle.ContMDiffRiemannianMetric.contMDiff, InnerProductSpace.isPositive_rankOne_self, mulLeftRight_isBoundedBilinear, MDifferentiableOn.clm_postcomp, compSL_apply, InnerProductSpace.rankOne_one_left_eq_innerSL, fderivWithin_fderivWithin_eq_of_mem_nhdsWithin, MDifferentiableAt.cle_arrowCongr, ProbabilityTheory.covarianceBilinDual_apply', InnerProductSpace.isIdempotentElem_rankOne_self, Differentiable.clm_comp, ProbabilityTheory.covarianceBilinDual_apply, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, ContMDiffOn.clm_postcomp, ProbabilityTheory.uncenteredCovarianceBilin_apply, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, fderiv_clm_comp, InnerProductSpace.inner_left_rankOne_apply, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, topologicalAddGroup, InnerProductSpace.rankOne_apply, HasStrictDerivAt.clm_comp, derivWithin_clm_comp, precompL_apply, MDifferentiable.clm_postcomp, toSesqForm_apply_coe, finiteDimensional, hasFDerivWithinAt_of_bilinear, MDifferentiable.cle_arrowCongr, fderiv_continuousAlternatingMapCompContinuousLinearMap, compactOperator_topologicalClosure, hasStrictFDerivAt_of_bilinear, Real.fourier_iteratedFDeriv, mulLeftRight_apply, MDifferentiableAt.clm_postcomp, hasFDerivAt_ringInverse, VectorFourier.fourierIntegral_iteratedFDeriv, InnerProductSpace.nnnorm_rankOne, InnerProductSpace.isSymmetricProjection_rankOne_self, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, NormedSpace.inclusionInDoubleDual_norm_eq, fderiv_of_bilinear, norm_smulRightL, InnerProductSpace.trace_rankOne, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, compL_apply, NormedSpace.toLinearMap_inclusionInDoubleDualWeak, isUniformAddGroup, fderiv_inverse, ContMDiffOn.clm_precomp, InnerProductSpace.adjoint_rankOne, InnerProductSpace.rankOne_eq_zero, InnerProductSpace.inner_right_rankOne_apply, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_inv', fderivWithin_of_bilinear, NormedSpace.inclusionInDoubleDual_norm_le, InnerProductSpace.rankOne_eq_rankOne_iff_comm, precompR_apply, ProbabilityTheory.covarianceBilinDual_eq_covariance, ProbabilityTheory.covarianceBilinDual_zero, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, ContinuousAffineMap.fst_decompAffineEquiv, IsContMDiffRiemannianBundle.exists_contMDiff, InnerProductSpace.rank_rankOne, ContMDiffOn.cle_arrowCongr, adjointAux_apply, InnerProductSpace.rankOne_def, fderivWithin_fderivWithin_eq_of_mem_nhds, DifferentiableOn.clm_comp, coe_flipMultilinearEquiv, TopModuleCat.hom_zsmul, fderivWithin_fderivWithin_eq_of_eventuallyEq, norm_precompR_le, Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange, IsContinuousRiemannianBundle.exists_continuous, contMDiffOn_continuousLinearMapCoordChange, InnerProductSpace.enorm_rankOne, Real.fourier_fderiv, ContinuousAffineMap.linear_decompAffineEquiv, HasDerivAt.clm_comp, NormedSpace.inclusionInDoubleDualWeak_apply, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, iteratedFDerivWithin_two_apply', PiTensorProduct.dualSeminorms_bounded, opNorm_mulLeftRight_apply_le, ProbabilityTheory.covarianceBilinDual_self_eq_variance, PiTensorProduct.injectiveSeminorm_apply, ProbabilityTheory.covarianceBilinDual_self_nonneg, ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ContMDiffAt.clm_precomp, ContinuousAffineMap.decompAffineEquiv_symm_apply, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, InnerProductSpace.rankOne_def', ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, DifferentiableWithinAt.clm_comp, MDifferentiableOn.cle_arrowCongr, MDifferentiableAt.clm_precomp, mdifferentiableOn_continuousLinearMapCoordChange, InnerProductSpace.isStarProjection_rankOne_self, HasFDerivWithinAt.clm_comp, evalL_apply, hasStrictFDerivAt_ringInverse, InnerProductSpace.rankOne_comp_rankOne, InnerProductSpace.rankOne_comp, Real.fourierIntegral_fderiv, InnerProductSpace.toMatrix_rankOne, InnerProductSpace.isSymmetric_rankOne_self, DifferentiableAt.clm_comp, fderiv_continuousLinearEquiv_comp, deriv_clm_comp, ProbabilityTheory.isPosSemidef_covarianceBilinDual, spectrum.hasFDerivAt_resolvent, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, fderiv_continuousMultilinearMapCompContinuousLinearMap, opNorm_mulLeftRight_apply_apply_le, TopModuleCat.hom_nsmul, norm_compL_le, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, fderivWithin_clm_comp, ProbabilityTheory.covarianceBilinDual_comm, ContMDiff.clm_postcomp, MDifferentiableWithinAt.clm_postcomp, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, MDifferentiableOn.clm_precomp, deriv_clm_apply, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, InnerProductSpace.toLinearMap_rankOne, iteratedFDerivWithin_two_apply, hasFDerivAt_of_bilinear, ProbabilityTheory.uncenteredCovarianceBilin_zero, fderiv_clm_apply, norm_compSL_le, InnerProductSpace.isIdempotentElem_rankOne_self_iff, fderivWithin_continuousLinearEquiv_comp, OrthonormalBasis.sum_rankOne_eq_id, norm_smulRightL_le, coe_symm_flipMultilinearEquiv, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, hasStrictFDerivAt_inv', iteratedFDeriv_two_apply, MDifferentiable.clm_precomp, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, opNorm_mulLeftRight_le, ContMDiffWithinAt.clm_precomp, ContinuousAffineMap.snd_decompAffineEquiv, ContMDiff.clm_precomp, ProbabilityTheory.covarianceBilinDual_of_not_memLp, NormedSpace.double_dual_bound, Real.zero_at_infty_vector_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, ContinuousAffineMap.decompAffineEquiv_symm_contLinear, ProbabilityTheory.IsGaussian.charFunDual_eq', hasFDerivAt_inv', exists_continuousLinearEquiv_fderiv_symm_eq, ContMDiffWithinAt.cle_arrowCongr, apply_apply', ProbabilityTheory.covarianceBilinDual_of_not_memLp', fderivWithin_clm_apply, exists_continuousLinearEquiv_fderivWithin_symm_eq, HasStrictFDerivAt.clm_comp, VectorFourier.fourierIntegral_fderiv, fderiv_continuousLinearEquiv_comp', smulRightL_apply_apply, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, apply_apply, IsSymmSndFDerivWithinAt.eq, Real.fourierIntegral_iteratedFDeriv, derivWithin_clm_apply, InnerProductSpace.symm_toEuclideanLin_rankOne, ContMDiffAt.cle_arrowCongr, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, HasFDerivAt.clm_comp, norm_smulRightL_apply, NormedSpace.dual_def, toSesqForm_apply_norm_le, PiTensorProduct.injectiveSeminorm_def, ContMDiff.cle_arrowCongr, InnerProductSpace.norm_rankOne, IsSymmSndFDerivAt.eq, fderiv_inv'
addCommMonoid 📖	CompOp	704 math math: LinearMap.det_toContinuousLinearMap, LinearMap.mkContinuous₂_norm_le', derivWithin_of_bilinear, Bundle.ContMDiffRiemannianMetric.isVonNBounded, LinearMap.mkContinuous₂_apply, isPositive_iff_eq_sum_rankOne, Bundle.ContMDiffRiemannianMetric.contMDiff, continuousOn_stereoToFun, InnerProductSpace.isPositive_rankOne_self, ProbabilityTheory.isGaussian_iff_gaussian_charFun, mulLeftRight_isBoundedBilinear, HasFDerivWithinAt.continuousMultilinearMap_apply, MDifferentiableOn.clm_postcomp, analyticWithinAt_bilinear, HasCompactSupport.convolution_integrand_bound_left, compSL_apply, continuous₂, SchwartzMap.integral_sesq_fourier_fourier, Real.hasFDerivAt_fourierChar_neg_bilinear_left, MeasureTheory.convolution_eq_right', hasStrictFDerivAt_list_prod_finRange', MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, InnerProductSpace.rankOne_one_left_eq_innerSL, map_add_add, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, toLinearMap₁₂_injective, hasFDerivAt_multiset_prod, MDifferentiableAt.cle_arrowCongr, ProbabilityTheory.covarianceBilinDual_apply', ContinuousAffineMap.fst_decompLinearEquiv, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, SchwartzMap.pairing_apply_apply, InnerProductSpace.isIdempotentElem_rankOne_self, StrongDual.polarSubmodule_eq_setOf, IsCovariantDerivativeOn.difference_apply, ProbabilityTheory.covarianceBilinDual_apply, Real.fderiv_fourierChar_neg_bilinear_right_apply, fderivWithin_fun_pow', HasFDerivWithinAt.clm_apply, Continuous.convolution_integrand_fst, iteratedFDerivWithin_succ_eq_comp_right, innerSL_apply_apply, fderiv_multiset_prod, ProbabilityTheory.covarianceBilin_multivariateGaussian, SchwartzMap.integral_bilin_fourierInv_eq, HasFDerivAtFilter.fun_sum, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, innerSL_apply_comp_of_isSymmetric, Unitization.splitMul_apply, ContMDiffOn.clm_postcomp, toBilinForm_apply, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, LinearMap.adjoint_eq_toCLM_adjoint, ProbabilityTheory.uncenteredCovarianceBilin_apply, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, opNorm_lsmul_apply_le, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, fderiv_clm_comp, SchwartzMap.bilinLeftCLM_apply, fpowerSeriesBilinear_apply_zero, fderiv_continuousAlternatingMap_apply_const, coprodEquiv_apply, Bundle.RiemannianMetric.isVonNBounded, ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, coe_restrictScalarsₗ, 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, LinearMap.coe_toContinuousLinearMap', HasFDerivWithinAt.linear_multilinear_comp, CStarModule.innerSL_apply, hasDerivWithinAt_of_bilinear, Bundle.ContinuousLinearMap.vectorBundle, MeasureTheory.ConvolutionExistsAt.integrable, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, opNorm_mul_flip_apply, bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, InnerProductSpace.inner_left_rankOne_apply, HasFDerivAt.finset_prod, HasStrictFDerivAt.fun_sum, HasFDerivAt.norm_sq, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, fderiv_fun_pow', Real.integrable_prod_sub, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, sum_apply, HasFDerivAt.continuousMultilinear_apply_const, HasFDerivWithinAt.continuousAlternatingMap_apply, InnerProductSpace.rankOne_apply, fderiv_sum, NormedSpace.Dual.toWeakDual_continuous, mkOfIsCompactOperator_mem_compactOperator, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMultilinearMap.norm_smulRightL_le, precompL_apply, MDifferentiable.clm_postcomp, CStarMatrix.toCLM_injective, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, LinearMap.adjoint_toContinuousLinearMap, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, toSesqForm_apply_coe, HasFDerivAt.multilinear_comp, SchwartzMap.integral_bilin_fourierIntegral_eq, toLinearMap₁₂_apply, VectorFourier.fourierPowSMulRight_eq_comp, hasFDerivWithinAt_of_bilinear, HasFDerivWithinAt.multiset_prod, opNorm_mul, MDifferentiable.cle_arrowCongr, flipMultilinear_apply_apply, fderiv_continuousAlternatingMapCompContinuousLinearMap, compactOperator_topologicalClosure, SchwartzMap.integral_sesq_fourier_eq, adjointAux_norm, MDifferentiable.clm_bundle_apply₂, ProbabilityTheory.covarianceBilin_apply_basisFun_self, hasStrictFDerivAt_of_bilinear, HasStrictFDerivAt.list_prod', LinearMap.toContinuousBilinearMap_apply, CStarMatrix.inner_toCLM_conjTranspose_left, Real.fourier_iteratedFDeriv, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable, WeakDual.toStrongDual_inj, mulLeftRight_apply, LinearMap.dualEmbedding_surjective, Bundle.ContinuousRiemannianMetric.symm, ContinuousMultilinearMap.curryRight_norm, analyticOn_bilinear, hasStrictFDerivAt_multiset_prod, continuous_of_continuous_uncurry, MDifferentiableAt.clm_postcomp, fderiv_continuousAlternatingMap_apply, coe_innerSL_apply, fderivWithin_finset_prod, RegularNormedAlgebra.isometry_mul', HasFDerivAt.sum, IsCovariantDerivativeOn.torsion_self, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, MDifferentiableWithinAt.clm_bundle_apply₂, ContinuousAffineMap.decompLinearEquiv_symm_contLinear, HasFDerivAt.clm_apply, StrongDual.toWeakDual_inj, hasFDerivAt_ringInverse, HasFDerivAt.continuousAlternatingMap_apply, WeakDual.coe_toStrongDual, VectorFourier.fourierIntegral_iteratedFDeriv, InnerProductSpace.nnnorm_rankOne, ContinuousLinearEquiv.arrowCongr_apply, toUniformConvergenceCLM_apply, flip_smul, InnerProductSpace.isSymmetricProjection_rankOne_self, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, MeasureTheory.ConvolutionExistsAt.integrable_swap, ContMDiffCovariantDerivativeOn.finite_affine_combination, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, instLocallyConvexSpace, NormedSpace.inclusionInDoubleDual_norm_eq, SchwartzMap.smulLeftCLM_sum, ContinuousAffineMap.decompLinearIsometryEquiv_symm_apply, fderiv_of_bilinear, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, CovariantDerivative.torsion_apply, IsCovariantDerivativeOn.torsion_antisymm, LinearMap.toLinearMap_toContPerfPair, opNorm_mul_apply, norm_smulRightL, NormedSpace.inclusionInDoubleDualWeak_apply_apply, MeasureTheory.convolution_def, compContinuousMultilinearMapL_apply, InnerProductSpace.trace_rankOne, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, SchwartzMap.fourierMultiplierCLM_sum, ContMDiffVectorBundle.continuousLinearMap, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, hasFDerivAt_norm_rpow, compL_apply, lsmul_flip_inj, summable_jacobiTheta₂_term_fderiv_iff, 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, InnerProductSpace.inner_right_rankOne_apply, SchwartzMap.pairing_apply, innerSL_inj, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_inv', MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, StrongDual.toLp_of_not_memLp, fderivWithin_of_bilinear, NormedSpace.inclusionInDoubleDual_norm_le, WeakDual.isCompact_closedBall, Convex.second_derivative_within_at_symmetric, BoxIntegral.BoxAdditiveMap.volume_apply, InnerProductSpace.rankOne_eq_rankOne_iff_comm, precompR_apply, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd', ProbabilityTheory.IsGaussian.charFun_eq', fderiv_pow', ProbabilityTheory.covarianceBilinDual_eq_covariance, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ProbabilityTheory.covarianceBilinDual_zero, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, Bundle.Pretrivialization.continuousLinearMap.isLinear, hasStrictDerivAt_of_bilinear, ContinuousLinearEquiv.arrowCongr_symm, isBoundedBilinearMap, fderivWithin_continuousMultilinear_apply_const, ContinuousAffineMap.fst_decompAffineEquiv, continuousMultilinearCurryRightEquiv_symm_apply, coe_smulRightₗ, lsmul_apply, Bundle.ContMDiffRiemannianMetric.pos, bilinearComp_zero_right, IsContMDiffRiemannianBundle.exists_contMDiff, comp_finset_sum, InnerProductSpace.rank_rankOne, ContMDiffOn.cle_arrowCongr, Convex.taylor_approx_two_segment, adjointAux_apply, ProperCone.innerDual_singleton, hasFDerivAt_list_prod', InnerProductSpace.rankOne_def, coe_flipₗᵢ', MDifferentiableAt.clm_bundle_apply₂, stereoToFun_apply, adjointAux_inner_left, SchwartzMap.convolution_apply, hasSum_jacobiTheta₂_term_fderiv, ProbabilityTheory.covarianceBilin_comm, HasFDerivAtFilter.sum, SchwartzMap.integral_bilin_fourier_eq, 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, coe_restrict_scalarsL', StrongDual.polarSubmodule_eq_polar, PiTensorProduct.liftEquiv_symm_apply, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, norm_iteratedFDeriv_le_of_bilinear, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, aestronglyMeasurable_comp₂, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt, fderiv_fun_sum, ContinuousAffineMap.decompLinearIsometryEquiv_symm_contLinear, LinearMap.range_toContinuousLinearMap, norm_precompR_le, hasFDerivWithinAt_pow', hasFPowerSeriesOnBall_bilinear, WeakDual.isSeqCompact_closedBall, PiTensorProduct.liftEquiv_apply, 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, LinearMap.coe_toContinuousLinearMap, prodMapL_apply, toSpanSingletonLE_apply, IsBilinearMap.toContinuousBilinearMap_apply, contMDiffOn_continuousLinearMapCoordChange, InnerProductSpace.enorm_rankOne, InnerProductSpace.continuousLinearMapOfBilin_zero, ContinuousMultilinearMap.compContinuousLinearMapLRight_apply, toLinearMap_innerSL_apply, hasFDerivAt_list_prod_finRange', ContinuousMultilinearMap.flipLinear_apply_apply, CStarMatrix.toCLM_apply_single, Real.fourier_fderiv, ContinuousAffineMap.linear_decompAffineEquiv, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, HasFDerivWithinAt.norm_sq, StrongDual.dualPairing_separatingLeft, ProperCone.dual_singleton, uncurryBilinear_apply, StrongDual.extendRCLikeₗ_apply, MeasureTheory.integral_posConvolution, VectorFourier.integral_fourierIntegral_swap, NormedSpace.inclusionInDoubleDualWeak_apply, Bundle.RiemannianMetric.symm, LinearMap.toContinuousLinearMap_eq_iff_eq_toLinearMap, Unitization.norm_eq_sup, CStarMatrix.toCLM_apply_eq_sum, coeLM_apply, LinearMap.isPositive_toContinuousLinearMap_iff, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff, HasFDerivAt.multiset_prod, memLp_of_bilin, toLinearMap_eq_iff_eq_toContinuousLinearMap, 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, fderiv_pow_ring', map_sub₂, bilinearComp_apply, ContMDiffWithinAt.clm_bundle_apply₂, CStarMatrix.toCLM_apply, HasFDerivAt.continuousAlternatingMap_apply_const, ProbabilityTheory.covarianceBilinDual_self_nonneg, ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply, Matrix.l2_opNNNorm_def, adjointAux_adjointAux, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ContMDiffAt.clm_precomp, ProbabilityTheory.covarianceBilin_real_self, HasMFDerivWithinAt.sum, coprodEquivL_apply_apply, flip_add, VectorFourier.fourierSMulRight_apply, ContinuousMultilinearMap.uncurryRight_apply, bilinearComp_zero, HasFDerivAt.fun_pow', integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, WeakDual.isClosed_closedBall, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, ContinuousAffineMap.decompAffineEquiv_symm_apply, Real.fourier_bilin_convolution_eq, BoxIntegral.BoxAdditiveMap.toSMul_apply, CStarMatrix.mul_entry_mul_eq_inner_toCLM, le_opNorm₂, lpPairing_eq_integral, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, InnerProductSpace.rankOne_def', opNorm_mul_le, HasFDerivWithinAt.multilinear_comp, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, SchwartzMap.integral_sesq_fourierIntegral_eq, MeasureTheory.Integrable.convolution_integrand, ProbabilityTheory.covarianceBilin_apply_pi, SchwartzMap.integral_bilinear_laplacian_right_eq_left, isometry_mul, StrongDual.toLpₗ_apply, HasStrictFDerivAt.continuousAlternatingMap_apply, tendsto_iff_forall_eval_tendsto_topDualPairing, StrongDual.extendRCLikeₗ_symm_apply, MeasureTheory.dist_convolution_le', fderivWithin_multiset_prod, CovariantDerivative.torsion_eq_zero_iff, MDifferentiableOn.cle_arrowCongr, InnerProductSpace.innerSL_norm, ContMDiff.clm_bundle_apply₂, IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt, second_derivative_symmetric, ContinuousMultilinearMap.curryRight_apply, hasStrictFDerivAt_pow', MDifferentiableAt.clm_precomp, ProbabilityTheory.covarianceBilin_apply_basisFun, ContinuousMultilinearMap.analyticOn_uncurry_of_linear, mdifferentiableOn_continuousLinearMapCoordChange, InnerProductSpace.isStarProjection_rankOne_self, LinearMap.mkContinuous₂_norm_le, hasFPowerSeriesAt_bilinear, fderiv_finset_prod, hasStrictFDerivAt_list_prod_attach', StrongDual.norm_toLpₗ_le, WeakDual.isBounded_toWeakDual_preimage_iff_isBounded, PiTensorProduct.mapLMultilinear_apply_apply, HasFDerivWithinAt.clm_comp, evalL_apply, hasStrictFDerivAt_ringInverse, mul_apply', HasFDerivAt.fun_sum, InnerProductSpace.rankOne_comp_rankOne, BoxIntegral.hasIntegral_const, StrongDual.toLpₗ_of_not_memLp, hasStrictFDerivAt_finset_prod, InnerProductSpace.rankOne_comp, StrongDual.mem_polarSubmodule, Real.fourierIntegral_fderiv, InnerProductSpace.toMatrix_rankOne, HasFDerivWithinAt.continuousMultilinear_apply_const, InnerProductSpace.isSymmetric_rankOne_self, opNNNorm_mul, norm_iteratedFDerivWithin_le_of_bilinear, iteratedFDeriv_succ_eq_comp_right, ContinuousAffineMap.snd_decompLinearIsometryEquiv, coe_sum', fderiv_continuousLinearEquiv_comp, SchwartzMap.convolution_continuous_left, adjoint_toSpanSingleton, toBilinForm_injective, spectrum.hasFDerivAt_resolvent, IsBoundedBilinearMap.toContinuousLinearMap_apply, HasFDerivWithinAt.pow', SchwartzMap.pairing_continuous_left, IsCovariantDerivativeOn.add_one_form, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, innerSLFlip_apply, ContinuousAt.clm_bundle_apply₂, HasFDerivAt.list_prod', ProbabilityTheory.covarianceBilin_real, separatingDual_iff_injective, fderiv_continuousMultilinearMapCompContinuousLinearMap, hasFDerivAt_pow', opNorm_mulLeftRight_apply_apply_le, opNorm_lsmul_le, ProbabilityTheory.covarianceBilin_of_not_memLp, WeakDual.CharacterSpace.norm_le_norm_one, 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, fderivWithin_clm_comp, HasStrictFDerivAt.sum, fderiv_continuousMultilinear_apply_const, ProbabilityTheory.covarianceBilinDual_comm, NormedSpace.isEmbedding_inclusionInDoubleDualWeak, opNNNorm_mul_flip_apply, CovariantDerivative.torsion_antisymm, HasMFDerivAt.prod, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, ContMDiff.clm_postcomp, fderivWithin_continuousAlternatingMap_apply_const, ContinuousLinearEquiv.arrowCongrSL_apply, MDifferentiableWithinAt.clm_postcomp, hasFDerivAt_uncurry_of_multilinear, opNorm_mul_apply_le, ProbabilityTheory.covarianceBilin_apply, BoxIntegral.integralSum_sub_partitions, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, MeasureTheory.convolutionExistsAt_iff_integrable_swap, hasFDerivAt_tsum, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, norm_bilinearRestrictScalars, coeLMₛₗ_apply, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, ProbabilityTheory.covarianceBilin_map, Unitization.nnnorm_eq_sup, bilinearComp_zero_left, Bundle.ContinuousRiemannianMetric.pos, Matrix.toLin_finTwoProd_toContinuousLinearMap, IsCoercive.continuousLinearEquivOfBilin_apply, MDifferentiableOn.clm_precomp, HasFDerivWithinAt.fun_sum, ContinuousAffineMap.decompLinearEquiv_symm_apply, VectorFourier.integral_bilin_fourierIntegral_eq_flip, InnerProductSpace.toLinearMap_rankOne, adjointAux_inner_right, Bundle.RiemannianMetric.pos, HasStrictFDerivAt.clm_apply, ContMDiffAt.clm_bundle_apply₂, continuousMultilinearCurryRightEquiv_symm_apply', ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, prodL_apply, LinearMap.isStarProjection_toContinuousLinearMap_iff, DoubleCentralizer.coe_fst, HasFDerivAt.pow', HasStrictFDerivAt.pow', hasFDerivAt_of_bilinear, ProbabilityTheory.uncenteredCovarianceBilin_zero, HasStrictFDerivAt.multiset_prod, LinearMap.toContPerfPair_apply, TensorialAt.mkHom₂_apply, VectorFourier.fourierPowSMulRight_apply, SchwartzMap.convolution_flip, opNorm_flip, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, WeakDual.isBounded_toStrongDual_preimage_iff_isBounded, StrongDual.toWeakDual_apply, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub, TemperedDistribution.fourierMultiplierCLM_sum, BoxIntegral.integral_const, FormalMultilinearSeries.derivSeries_eq_zero, norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, fderivWithin_list_prod', fderiv_clm_apply, norm_compSL_le, 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, Continuous.clm_bundle_apply₂, fderivWithin_pow_ring', IsCovariantDerivativeOn.torsion_apply_eq_extend, Real.differentiable_fourierChar_neg_bilinear_right, OrthonormalBasis.sum_rankOne_eq_id, HasFDerivWithinAt.fun_pow', HasStrictFDerivAt.continuousAlternatingMap_apply_const, toSpanSingletonLE_symm_apply, MeasureTheory.condExp_bilin_of_stronglyMeasurable_right, CovariantDerivative.torsion_self, norm_smulRightL_le, ContinuousAffineMap.fst_decompLinearIsometryEquiv, coe_symm_flipMultilinearEquiv, VectorFourier.norm_fourierSMulRight_le, le_of_opNorm₂_le_of_le, coe_sum, WeakDual.isBounded_closedBall, signedDist_apply, HasStrictFDerivAt.fun_pow', continuousMultilinearCurryRightEquiv_apply', flipₗᵢ'_symm, flip_zero, VectorFourier.norm_fourierPowSMulRight_le, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, Real.hasFDerivAt_fourierChar_neg_bilinear_right, VectorFourier.norm_fourierSMulRight, fderivWithin_continuousAlternatingMap_apply, toUniformConvergenceCLM_continuous, hasStrictFDerivAt_inv', HasMFDerivAt.sum, LinearMap.dualEmbedding_injective_of_separatingRight, SchwartzMap.fourier_convolution_apply, TemperedDistribution.smulLeftCLM_sum, StrongDual.coe_toWeakDual, WeakDual.toStrongDual_apply, MDifferentiable.clm_precomp, Real.differentiable_fourierChar_neg_bilinear_left, ContinuousAffineMap.snd_decompLinearEquiv, ContinuousMultilinearMap.smulRightL_apply, Convex.second_derivative_within_at_symmetric_of_mem_interior, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, CovariantDerivative.torsion_apply_eq_extend, ContinuousLinearEquiv.arrowCongrSL_symm_apply, opNorm_mulLeftRight_le, topDualPairing_apply, ContMDiffWithinAt.clm_precomp, LinearMap.coe_toContinuousLinearMap_symm, HasFDerivWithinAt.finset_prod, hasStrictFDerivAt_list_prod', MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound, Submodule.orthogonal_eq_inter, lsmul_flip_apply, compContinuousAlternatingMapCLM_apply_apply, prodₗ_apply, coprodEquiv_symm_apply, fderiv_norm_rpow, map_add₂, ContinuousAffineMap.snd_decompAffineEquiv, MeasureTheory.integral_bilinear_hasDerivAt_eq_sub, ContMDiff.clm_precomp, FormalMultilinearSeries.derivSeries_apply_diag, opNorm_lsmul, ProbabilityTheory.covarianceBilinDual_of_not_memLp, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, 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, ContinuousAffineMap.decompAffineEquiv_symm_contLinear, precomp_apply, norm_holderL_le, ContinuousAffineMap.toConstProdContinuousLinearMap_fst, 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, isPositive_sum, toUniformConvergenceCLM_symm_apply, integral_bilinear_fderiv_right_eq_neg_left_of_integrable, hasFDerivAt_inv', TensorialAt.mkHom₂_apply_eq_extend, MeasureTheory.AEStronglyMeasurable.convolution_integrand', map_neg₂, Matrix.l2_opNorm_def, 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', fderiv_list_prod', SchwartzMap.fourier_convolution, HasMFDerivWithinAt.prod, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, flipₗᵢ_symm, fderivWithin_clm_apply, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, norm_holder_apply_apply_le, fderivWithin_sum, ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, HasStrictFDerivAt.clm_comp, VectorFourier.fourierIntegral_fderiv, fderiv_continuousLinearEquiv_comp', smulRightL_apply_apply, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, toSpanSingletonCLE_apply_apply, HasStrictFDerivAt.continuousMultilinearMap_apply, opNNNorm_mul_apply, toSpanSingletonCLE_symm_apply, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, Real.fderiv_fourierChar_neg_bilinear_left_apply, apply_apply, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply, map_smulₛₗ₂, PiTensorProduct.mapLMultilinear_opNorm, hasFDerivAt_tsum_of_isPreconnected, instModuleFinite, fderivWithin_fun_sum, Real.fourierIntegral_iteratedFDeriv, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, hasFDerivAt_list_prod_attach', MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd, HasCompactSupport.convolution_integrand_bound_right, InnerProductSpace.symm_toEuclideanLin_rankOne, ContMDiffAt.cle_arrowCongr, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, HasFDerivAt.clm_comp, adjoint_innerSL_apply, Bundle.Pretrivialization.continuousLinearMapCoordChange_apply, fderiv_tsum_apply, coprodEquivL_symm_apply, HasCompactSupport.convolution_integrand_bound_right_of_subset, second_derivative_symmetric_of_eventually_of_real, toWOT_apply, norm_smulRightL_apply, SchauderBasis.sum_succSub, DoubleCentralizer.coe_snd, opNorm_le_bound₂, fpowerSeriesBilinear_apply_one, MeasureTheory.integral_convolution, fderiv_norm_sq_apply, NormedSpace.dual_def, fderiv_norm_sq, IsCovariantDerivativeOn.finite_affine_combination, coe_mulₗᵢ, MDifferentiableOn.clm_bundle_apply₂, HasFDerivWithinAt.continuousAlternatingMap_apply_const, innerSL_apply_comp, toSesqForm_apply_norm_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd, coeFn_holder, CStarMatrix.norm_def, ContMDiff.cle_arrowCongr, coe_deriv₂, ContMDiffOn.clm_bundle_apply₂, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply, Bundle.ContinuousRiemannianMetric.isVonNBounded, HasFDerivWithinAt.sum, hasDerivAt_of_bilinear, second_derivative_symmetric_of_eventually, HasStrictFDerivAt.finset_prod, InnerProductSpace.norm_rankOne, PiTensorProduct.mapLMultilinear_toFun_apply, CStarMatrix.inner_toCLM_conjTranspose_right, ContinuousAffineMap.toConstProdContinuousLinearMap_snd, CStarMatrix.toCLM_apply_single_apply, ContinuousMultilinearMap.uncurryRight_norm, flipAlternating_apply_apply, LinearMap.ker_toContinuousLinearMap, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable, norm_iteratedFDerivWithin_le_of_bilinear_aux, HasFDerivWithinAt.list_prod', HasFDerivAt.continuousMultilinearMap_apply, finset_sum_comp, fderiv_inv', fderivWithin_pow', hasFDerivAt_finset_prod
algebra 📖	CompOp	31 math math: ContinuousLinearEquiv.conjContinuousAlgEquiv_refl, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, Unitization.splitMul_apply, ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective, Unitization.nnnorm_def, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, ContinuousLinearEquiv.conjContinuousAlgEquiv_trans, Unitization.splitMul_injective_of_clm_mul_injective, VonNeumannAlgebra.centralizer_centralizer', IsCompactOperator.hasEigenvalue_or_mem_resolventSet, VonNeumannAlgebra.coe_mk, VonNeumannAlgebra.mem_carrier, Unitization.norm_eq_sup, DoubleCentralizer.algebraMap_snd, DoubleCentralizer.algebraMap_toProd, PositiveLinearMap.gnsStarAlgHom_apply, Algebra.IsCentral.instContinuousLinearMap, Unitization.norm_def, DoubleCentralizer.algebraMap_fst, spectralRadius_eq_nnnorm, spectrum_eq, Unitization.nnnorm_eq_sup, VonNeumannAlgebra.coe_toStarSubalgebra, Unitization.norm_splitMul_snd_sq, Unitization.splitMul_injective, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply, algebraMap_apply
applyModule 📖	CompOp	5 math math: applySMulCommClass', applyFaithfulSMul, applySMulCommClass, smul_def, continuousConstSMul_apply
codRestrict 📖	CompOp	4 math math: ker_codRestrict, coe_codRestrict, coe_codRestrict_apply, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap
coeLM 📖	CompOp	2 math math: coeLM_apply, separatingDual_iff_injective
coeLMₛₗ 📖	CompOp	1 math math: coeLMₛₗ_apply
comp 📖	CompOp	388 math math: comp_neg, sum_comp_single, HasDerivWithinAt.clm_comp, SchwartzMap.lineDerivOpCLM_eq, ClosedSubmodule.comap_comap, LinearIsometryEquiv.comp_fderiv, HasFDerivWithinAt.continuousMultilinearMap_apply, compSL_apply, HasRightInverse.comp_continuousLinearEquivalence, snd_comp_inr, Continuous.clm_comp_const, Real.hasFDerivAt_fourierChar_neg_bilinear_left, coe_comp', HasRightInverse.continuousLinearEquivalence_comp, Submodule.IsOrtho.starProjection_comp_starProjection, ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, SeparationQuotient.mkCLM_comp_outCLM, Differentiable.clm_comp, precompUniformConvergenceCLM_apply, LinearIsometryEquiv.comp_fderivWithin, HasFDerivWithinAt.clm_apply, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, innerSL_apply_comp_of_isSymmetric, mfderiv_comp, opNorm_comp_linearIsometryEquiv, ContinuousLinearEquiv.coe_comp_coe_symm, fderiv_clm_comp, coprod_comp_prodComm, IsConformalMap.is_complex_or_conj_linear, Differentiable.fderiv_norm_rpow, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, comp_inl_add_comp_inr, HasFDerivWithinAt.linear_multilinear_comp, Submodule.starProjection_comp_starProjection_eq_zero_iff, LinearIsometryEquiv.conjStarAlgEquiv_apply, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivWithinAt.comp_of_tendsto, bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, HasFDerivWithinAt.fst, isInvertible_comp_equiv, HasFDerivAt.norm_sq, Continuous.clm_comp, IsInvertible.inverse_comp_of_right, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, ContinuousLinearEquiv.comp_hasFDerivAt_iff, IsInvertible.inverse_comp_of_left, HasFDerivWithinAt.continuousAlternatingMap_apply, HasStrictDerivAt.clm_comp, derivWithin_clm_comp, Bundle.Pretrivialization.continuousLinearMap_apply, HasStrictFDerivAt.star, RKHS.kernel_apply, HasLeftInverse.comp_continuousLinearEquivalence, mfderiv_comp_of_eq, HasFDerivAt.star, isPositive_self_comp_adjoint, hasStrictFDerivAt_pi', HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, toSesqForm_apply_coe, inTangentCoordinates_eq_mfderiv_comp, HasFDerivAt.multilinear_comp, SchwartzMap.fourierMultiplierCLM_compL_fourierMultiplierCLM, Submodule.IsOrtho.orthogonalProjection_comp_subtypeL, hasFDerivWithinAt_pi', fderivWithin_star, PointwiseConvergenceCLM.postcomp_apply, fst_comp_prod, fderiv_continuousAlternatingMapCompContinuousLinearMap, Submodule.coe_orthogonalDecomposition_symm, isEmbedding_postcomp, MeasureTheory.charFunDual_pi', smul_comp, comp_add, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, isBoundedBilinearMap_comp, ContinuousAffineMap.comp_contLinear, HasMFDerivAt.smul, fderiv_continuousAlternatingMap_apply, HasFDerivAt.clm_apply, det_pi, HasFDerivAt.continuousAlternatingMap_apply, hasFDerivAt_finCons, hasFDerivWithinAt_finCons, HasFDerivWithinAt.star, HasStrictFDerivAt.fst, ContinuousOn.clm_comp, apply_norm_sq_eq_inner_adjoint_left, MeasureTheory.charFunDual_prod, HasFDerivAt.comp_hasFDerivWithinAt, mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff', mfderiv_prod_eq_add_comp, intrinsicStar_comp, mfderiv_comp_mfderivWithin, ContinuousLinearEquiv.comp_fderiv, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, ContinuousLinearEquiv.comp_right_fderiv, compL_apply, IsPositive.conj_adjoint, MeasureTheory.charFunDual_eq_prod_iff, exists_right_inverse_of_surjective, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, ContinuousWithinAt.clm_comp, coprod_comp_inl_inr, HasFDerivWithinAt.inner, InnerProductSpace.comp_rankOne, fderivWithin.snd, apply_norm_eq_sqrt_inner_adjoint_right, prod_ext_iff, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, inTangentCoordinates_eq, toContinuousAddMonoidHom_comp, comp_finset_sum, ContinuousLinearEquiv.coe_symm_comp_coe, inner_map_map_iff_adjoint_comp_self, ContinuousLinearEquiv.eq_toContinuousLinearMap_symm_comp, HasRightInverse.comp, isUniformInducing_postcomp, hasStrictFDerivAt_finCons, DifferentiableOn.clm_comp, fderiv_comp_fderivWithin, toSpanSingleton_comp, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain, Submodule.coe_orthogonalDecomposition, zero_comp, ContinuousLinearEquiv.comp_coe, ContMDiffOn.clm_comp, fromTangentSpace_mfderiv_smul', HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, SchwartzMap.postcompCLM_postcompCLM, hasStrictFDerivAt_piLp, isBoundedLinearMap_comp_right, ContDiffWithinAt.clm_comp, coe_comp, UpperHalfPlane.smulFDeriv_J_mul, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, postcomp_apply, opNorm_comp_le, comp_coprod, HasFDerivWithinAt.norm_sq, hasFDerivWithinAt_piLp, MDifferentiableAt.clm_comp, HasDerivAt.clm_comp, SeparationQuotient.exists_out_continuousLinearMap, mfderivWithin_comp_of_preimage_mem_nhdsWithin, PiTensorProduct.mapL_comp, ContinuousLinearEquiv.comp_right_hasFDerivAt_iff, fderiv.snd, OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, Bundle.Pretrivialization.continuousLinearMap_symm_apply, isometry_iff_adjoint_comp_self, postcompCompactConvergenceCLM_apply, IsSelfAdjoint.conj_adjoint, ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff', ProbabilityTheory.indepFun_iff_charFunDual_prod', ContinuousLinearEquiv.comp_right_fderivWithin, fderivWithin_comp_of_eq, sub_comp, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, ker_self_comp_adjoint, IsInvertible.comp, isBoundedLinearMap_comp_left, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ContDiffOn.clm_comp, intrinsicStar_eq_comp, LinearIsometry.norm_toContinuousLinearMap_comp, Submodule.sndL_comp_coe_orthogonalDecomposition, eventually_norm_symmL_trivializationAt_self_comp_lt, MeasureTheory.integral_continuousLinearMap_prod, fderivWithin_comp', ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, HasFDerivAtFilter.comp, StrongDual.extendRCLikeₗᵢ_symm_apply, InnerProductSpace.rankOne_def', ContDiff.clm_comp, HasFDerivWithinAt.multilinear_comp, ProbabilityTheory.iIndepFun_iff_charFunDual_pi, apply_norm_eq_sqrt_inner_adjoint_left, HasFDerivAt.inner, HasFDerivAtFilter.star, HasStrictFDerivAt.continuousAlternatingMap_apply, StrongDual.extendRCLikeₗ_symm_apply, isInducing_postcomp, MeasureTheory.integral_continuousLinearMap_prod', DifferentiableWithinAt.clm_comp, SeparationQuotient.postcomp_mkCLM_surjective, HasFDerivAtFilter.fst, eventually_norm_symmL_trivializationAt_comp_self_lt, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff', fderivWithin_comp₃, HasFDerivWithinAt.snd, UniformConvergenceCLM.isUniformEmbedding_postcomp, IsContDiffImplicitAt.bijective, opENorm_comp_le, snd_comp_prod, fderivWithin_comp_of_eq', ContDiffAt.hasStrictFDerivAt_implicitFunction, PointwiseConvergenceCLM.precomp_apply, HasFDerivWithinAt.comp, fderiv_comp, fst_comp_inl, HasFDerivAt.snd, hasFDerivWithinAt_euclidean, HasFDerivWithinAt.clm_comp, fst_comp_inr, Continuous.const_clm_comp, fromTangentSpace_mfderiv_smul, InnerProductSpace.rankOne_comp_rankOne, comp_smulₛₗ, isConformalMap_complex_linear_conj, InnerProductSpace.rankOne_comp, MDifferentiableWithinAt.clm_comp, hasFDerivAtFilter_finCons, PiTensorProduct.liftIsometry_comp_mapL, pi_comp, MDifferentiableOn.clm_comp, toSpanSingleton_comp_toSpanSingleton, precomp_compactConvergenceCLM_apply, HasFDerivAtFilter.snd, MeasureTheory.charFunDual_eq_pi_iff, ContinuousLinearEquiv.comp_hasFDerivAt_iff', DifferentiableAt.clm_comp, HasLeftInverse.comp, fderiv_continuousLinearEquiv_comp, deriv_clm_comp, Bundle.Trivialization.continuousLinearMap_apply, proj_pi, ker_adjoint_comp_self, smulRight_comp_smulRight, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, fderiv_continuousMultilinearMapCompContinuousLinearMap, HasFDerivAt.fst, inverse_comp_equiv, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, HasMFDerivAt.comp_hasMFDerivWithinAt, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, fderivWithin_clm_comp, inCoordinates_eq, ProbabilityTheory.variance_dual_prod', ProbabilityTheory.iIndepFun_iff_charFunDual_pi', mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', IsIdempotentElem.range_mem_invtSubmodule_iff, IsInvertible.inverse_comp_self, opNNNorm_comp_le, comp_zero, ContinuousLinearEquiv.arrowCongrEquiv_symm_apply, ContDiffAt.clm_comp, ContinuousLinearEquiv.arrowCongrSL_apply, hasFDerivAt_uncurry_of_multilinear, IsSelfAdjoint.conj_starProjection, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, MeasureTheory.charFunDual_prod', HasFDerivWithinAt.comp_hasFDerivAt_of_eq, neg_comp, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, fderiv_comp', intrinsicStar_comp', comp_assoc, VectorBundleCore.inCoordinates_eq, adjoint_comp, IsConformalMap.comp, IsInvertible.inverse_comp_apply_of_right, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, HasStrictFDerivAt.clm_apply, fderiv.fst, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, ContinuousLinearEquiv.arrowCongrEquiv_apply, IsPositive.orthogonalProjection_comp, MeasureTheory.charFunDual_eq_pi_iff', inverse_equiv_comp, LinearIsometryEquiv.comp_hasFDerivAt_iff', coprod_comp_inr, IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule, precompCompactConvergenceCLM_apply, IsPositive.adjoint_conj, PositiveLinearMap.leftMulMapPreGNS_mul_eq_comp, exist_extension_of_finiteDimensional_range, LinearIsometryEquiv.comp_hasFDerivAt_iff, inverse_eq_ringInverse, fderiv_clm_apply, fderiv_star, fderivWithin_continuousLinearEquiv_comp, snd_comp_inl, FormalMultilinearSeries.compContinuousLinearMap_comp, Submodule.fstL_comp_coe_orthogonalDecomposition, IsSelfAdjoint.adjoint_conj, HasLeftInverse.continuousLinearEquivalence_comp, HasFDerivAt.comp_semilinear, id_comp, Bundle.Pretrivialization.continuousLinearMap_symm_apply', mul_def, fderivWithin.fst, MeasureTheory.charFunDual_map, pi_proj_comp, IsPositive.conj_starProjection, HasStrictFDerivAt.comp, mfderiv_smul, ProbabilityTheory.variance_dual_prod, VectorBundleCore.coordChange_linear_comp, ContinuousAt.clm_comp, Real.hasFDerivAt_fourierChar_neg_bilinear_right, isUniformEmbedding_postcomp, smulRight_comp, fderivWithin_continuousAlternatingMap_apply, MeasureTheory.charFunDual_pi, add_comp, MDifferentiable.clm_comp, ContMDiff.clm_comp, coprod_comp_inl, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff, ContinuousLinearEquiv.arrowCongrSL_symm_apply, ProperCone.comap_comap, comp_sub, ContinuousLinearEquiv.comp_fderivWithin, coprodEquiv_symm_apply, norm_map_iff_adjoint_comp_self, norm_adjoint_comp_self, ContMDiffWithinAt.clm_comp, IsInvertible.self_comp_inverse, TopModuleCat.hom_comp, precomp_apply, SchwartzMap.smulLeftCLM_compL_smulLeftCLM, precomp_uniformConvergenceCLM_apply, HasMFDerivWithinAt.comp, postcompUniformConvergenceCLM_apply, Submodule.starProjection_comp_starProjection_of_le, ContinuousLinearEquiv.comp_right_hasFDerivAt_iff', apply_norm_sq_eq_inner_adjoint_right, bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasStrictFDerivAt.inner, HasMFDerivAt.comp, Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff, exists_continuousLinearEquiv_fderiv_symm_eq, isPositive_adjoint_comp_self, comp_fst_add_comp_snd, isInvertible_equiv_comp, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply, HasFDerivAt.star_star, fderivWithin_clm_apply, postcomp_uniformConvergenceCLM_apply, exists_continuousLinearEquiv_fderivWithin_symm_eq, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, hasFDerivAtFilter_pi', fderivWithin_comp, ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, HasStrictFDerivAt.clm_comp, HasFDerivWithinAt.comp_hasFDerivAt, fderiv_continuousLinearEquiv_comp', ContMDiffAt.clm_comp, HasStrictFDerivAt.continuousMultilinearMap_apply, IsInvertible.inverse_comp_apply_of_left, UniformConvergenceCLM.isUniformInducing_postcomp, mfderiv_comp_mfderivWithin_of_eq, isConformalMap_iff_is_complex_or_conj_linear, hasFDerivAt_pi', ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, MeasureTheory.charFunDual_eq_prod_iff', ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, HasFDerivAt.clm_comp, IsIdempotentElem.ker_mem_invtSubmodule_iff, coprodEquivL_symm_apply, LinearIsometryEquiv.comp_fderiv', postcomp_compactConvergenceCLM_apply, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, comp_id, innerSL_apply_comp, LinearIsometryEquiv.comp_hasStrictFDerivAt_iff, comp_toSpanSingleton, mfderivWithin_comp, IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule, HasFDerivAt.comp, ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff, lp.ext_continuousLinearMap_iff, comp_smul, comp_apply, ProbabilityTheory.indepFun_iff_charFunDual_prod, HasFDerivAt.continuousMultilinearMap_apply, finset_sum_comp, HasStrictFDerivAt.snd, hasStrictFDerivAt_euclidean, LinearIsometry.adjoint_comp_self, mfderivWithin_comp_of_eq
copy 📖	CompOp	2 math math: coe_copy, copy_eq
distribMulAction 📖	CompOp	10 math math: MeasureTheory.L1.setToL1_smul_left, CStarMatrix.norm_def', CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, flip_smul, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, NonUnitalAlgHom.coe_Lmul, MeasureTheory.setToFun_smul_left, PositiveLinearMap.gnsStarAlgHom_apply, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply
funLike 📖	CompOp	1790 math math: IsLocalMaxOn.fderivWithin_nonpos, MeasureTheory.L1.setToL1_eq_setToL1', hasFDerivAt_iff_hasDerivAt, TestFunction.lineDerivCLM_apply_of_le, VectorBundleCore.toFiberBundleCore_coordChange, geometric_hahn_banach_open, ContinuousOn.clm_apply, ContinuousMap.toLp_inj, TopModuleCat.hom_cokerπ, Bundle.Trivialization.symm_continuousLinearEquivAt_eq, sum_comp_single, Submodule.starProjection_apply_eq_isComplProjection, MeasureTheory.Lp.toTemperedDistributionCLM_apply, inner_map_map_of_mem_unitary, MeasureTheory.LpToLpRestrictCLM_coeFn, hasFPowerSeriesOnBall, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, rightInverse_of_comp, derivWithin_of_bilinear, Bundle.ContMDiffRiemannianMetric.isVonNBounded, ContinuousLinearEquiv.equivOfInverse'_apply, TrivSqZeroExt.fstCLM_apply, MeasureTheory.condExpInd_of_measurable, cfcₙL_integral, LinearMap.mkContinuous₂_apply, le_of_opNorm_le_of_le, isPositive_iff_eq_sum_rankOne, continuousOn_stereoToFun, Submodule.coe_continuous_linearProjOfClosedCompl', InnerProductSpace.isPositive_rankOne_self, WithSeminorms.banach_steinhaus, isBigO_comp, ContinuousLinearEquiv.unitsEquiv_apply, ProbabilityTheory.isGaussian_iff_gaussian_charFun, mulLeftRight_isBoundedBilinear, IsCompactOperator.clm_comp, LinearMap.mkContinuousOfExistsBound_apply, RCLike.map_apply, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, OrthonormalBasis.orthogonalProjection_eq_sum, analyticWithinAt_bilinear, MeasureTheory.aestronglyMeasurable_condExpInd, HasCompactSupport.convolution_integrand_bound_left, compSL_apply, continuous₂, RCLike.geometric_hahn_banach_point_open, fderivWithin_comp_derivWithin_of_eq, IsSelfAdjoint.quasispectrumRestricts, integral_compLp, DoubleCentralizer.star_snd, MeasureTheory.Measure.addHaar_image_continuousLinearMap, RCLike.ofRealCLM_apply, SchwartzMap.integral_sesq_fourier_fourier, Real.hasFDerivAt_fourierChar_neg_bilinear_left, coe_comp', geometric_hahn_banach_point_point, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.convolution_eq_right', RCLike.reCLM_apply, MeasureTheory.L1.setToL1_indicatorConstLp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left, RCLike.separate_convex_open_set, exists_preimage_norm_le, Convex.norm_image_sub_le_of_norm_fderivWithin_le', SchauderBasis.RankOneDecomposition.proj_tendsto, MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, InnerProductSpace.rankOne_one_left_eq_innerSL, MDifferentiableAt.clm_bundle_apply, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, map_add_add, sSup_unit_ball_eq_norm, NormedSpace.Dual.isClosed_image_polar_of_mem_nhds, analyticWithinAt, complexOfReal_hasDerivWithinAt, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, curveIntegrable_segment, frontier_preimage, ProbabilityTheory.covarianceBilinDual_apply', sSup_unitClosedBall_eq_nnnorm, smul_apply, MeasureTheory.charFunDual_apply, IsPositive.inner_left_eq_inner_right, conformalAt_iff, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq, AnalyticAtWithin.compContinuousLinearMap, MeasureTheory.norm_condExpL2_le, IsLocalMaxOn.hasFDerivWithinAt_nonpos, ProbabilityTheory.IsGaussian.integrable_dual, SchwartzMap.pairing_apply_apply, InnerProductSpace.isIdempotentElem_rankOne_self, MeasureTheory.weightedSMul_apply, comp_condExp_comm, geometric_hahn_banach_open_point, continuous_integral_comp_L1, isBigOWith_sub, ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, ClosedSubmodule.mem_comap, TopModuleCat.hom_zero_apply, ContDiffAt.clm_apply, hasDerivAtFilter, comp_hasFiniteFPowerSeriesOnBall, Submodule.re_inner_starProjection_eq_normSq, WeakSpace.map_apply, VectorField.fderiv_apply_lieBracket, MeasureTheory.inner_condExpL2_left_eq_right, ContinuousMap.toLp_denseRange, IsCovariantDerivativeOn.difference_apply, toContinuousAddMonoidHom_add, AnalyticOnNhd.compContinuousLinearMap, integral_apply, Module.Basis.constrL_basis, precompUniformConvergenceCLM_apply, ProbabilityTheory.covarianceBilinDual_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, comp_memLp, Real.fderiv_fourierChar_neg_bilinear_right_apply, SchauderBasis.tendsto_proj, Real.fourier_continuousLinearMap_apply, ContinuousLinearEquiv.snd_equivOfRightInverse, toWeakSpaceCLM_bijective, HasFDerivWithinAt.clm_apply, HasFPowerSeriesOnBall.unshift, Continuous.convolution_integrand_fst, ContDiffMapSupportedIn.structureMapCLM_apply, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, tangentMap_snd, iteratedDerivWithin_vcomp_two, SchwartzMap.lineDerivOp_fourier_eq, HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq, innerSL_apply_apply, IsInvertible.surjective, ProbabilityTheory.covarianceBilin_multivariateGaussian, SchwartzMap.integral_bilin_fourierInv_eq, TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars, VectorField.fderiv_apply_lieBracket_of_isSymmSndFDerivAt, norm_iteratedFDerivWithin_clm_apply, innerSL_apply_comp_of_isSymmetric, Unitization.splitMul_apply, RCLike.geometric_hahn_banach_of_nonempty_interior_point, toBilinForm_apply, Measurable.apply_continuousLinearMap, Summable.mapL, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, map_zero, Submodule.orthogonalProjection_mem_subspace_eq_self, IsPositive.inner_nonneg_right, completeSpace_eqLocus, LinearMap.mkContinuous_apply, id_apply, HasFDerivWithinAt.hasLineDerivWithinAt, ProbabilityTheory.uncenteredCovarianceBilin_apply, StrongDual.norm_extendRCLike_bound, TemperedDistribution.lineDerivOp_fourier_eq, FormalMultilinearSeries.derivSeries_coeff_one, Submodule.starProjection_add_starProjection_orthogonal, opNorm_lsmul_apply_le, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, fderiv_clm_comp, ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian, SchwartzMap.bilinLeftCLM_apply, intCast_apply, InnerProductSpace.toDual_symm_apply, fpowerSeriesBilinear_apply_zero, GeneralSchauderBasis.tendsto_proj, nhds_zero_eq_of_basis, MeasureTheory.L1.SimpleFunc.setToL1SCLM_const, SmoothBumpCovering.exists_immersion_euclidean, cpolynomialAt, Submodule.starProjection_singleton, HasDerivAt.clm_apply, mfderiv_comp_apply_of_eq, comp_condExp_add_const_comm, Bundle.RiemannianMetric.isVonNBounded, measurable, ContDiffWithinAt.clm_apply, coe_smul', WithLp.sndL_apply, GeneralSchauderBasis.proj_apply, hasStrictFDerivAt_iff_isLittleOTVS, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, DifferentiableOn.clm_apply, ContMDiff.clm_apply, exposed_point_def, ProbabilityTheory.integral_continuousLinearMap_gaussianReal, Differentiable.fderiv_norm_rpow, fderivWithin_fderivWithin, FDerivMeasurableAux.le_of_mem_A, lintegral_fderiv_lineMap_eq_edist, isBigOWith_id, integrable_of_bilin_of_bdd_left, comp_inl_add_comp_inr, fderiv_comp_deriv, VectorField.mlieBracket_smul_left, norm_iteratedFDeriv_le_of_bilinear_of_le_one, ContDiffOn.clm_apply, opNNNorm_le_iff, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1, isometry_mul_flip, BoundedContinuousFunction.evalCLM_apply, inner_gradientWithin_right, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, HasStrictFDerivAt.comp_hasStrictDerivAt, LinearMap.coe_toContinuousLinearMap', HasFDerivWithinAt.linear_multilinear_comp, isStarNormal_iff_norm_eq_adjoint, SchwartzMap.laplacianCLM_eq, CStarModule.innerSL_apply, hasDerivWithinAt_of_bilinear, isCompact_image_coe_of_bounded_of_closed_image, MeasureTheory.ConvolutionExistsAt.integrable, ProbabilityTheory.covarianceOperator_apply, algebraMapCLM_coe, ContDiffAt.laplacian_CLM_comp_left, coe_zero', Distribution.IsVanishingOn.smulLeftCLM, opNorm_mul_flip_apply, ConvexOn.univ_sSup_of_countable_affine_eq, 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, HasLeftInverse.leftInverse_leftInverse, ofMemClosureImageCoeBounded_apply, SchwartzMap.fderivCLM_apply, Submodule.norm_starProjection_apply_le, TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, contMDiff, mdifferentiable, HasFDerivAt.norm_sq, VectorBundleCore.coordChange_self, LinearIsometry.map_starProjection', cfcL_apply, LinearIsometry.coe_toContinuousLinearMap, geometric_hahn_banach_compact_closed, eq_adjoint_iff, hasFDerivAt, Submodule.starProjection_tendsto_self, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, IntrinsicStar.isSelfAdjoint_iff_map_star, SchwartzMap.toLpCLM_apply, single_apply, toSpanSingleton_apply, LinearMap.IsSymmetric.directSum_decompose_apply, sum_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, InnerProductSpace.rankOne_apply, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, HarmonicAt.analyticAt_complex_partial, MeasureTheory.SimpleFunc.setToSimpleFunc_const, toSpanSingleton_apply_one, MeasureTheory.weightedSMul_nonneg, cfcₙ_eq_cfcₙL_mkD, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, precompL_apply, Submodule.reflection_apply, curveIntegralFun_segment, HasDerivWithinAt.clm_apply, coe_mkOfIsCompactOperator, RCLike.geometric_hahn_banach_closed_point, InnerProductSpace.gramSchmidt_def, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, hasFPowerSeriesAt, SeparatingDual.exists_eq_one, fderiv_eq_deriv_mul, Submodule.starProjection_inner_eq_zero, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, toSesqForm_apply_coe, coe_algebraMapCLM, cpolynomialOn_uncurry_of_multilinear, BoxIntegral.hasIntegral_GP_pderiv, ContinuousMultilinearMap.linearDeriv_apply, SchwartzMap.integral_bilin_fourierIntegral_eq, ContinuousAffineMap.decomp, ContinuousAlternatingMap.toAlternatingMap_curryLeft, toLinearMap₁₂_apply, sSup_sphere_eq_nnnorm, VectorFourier.fourierPowSMulRight_eq_comp, MeasureTheory.charFunDual_eq_charFun_map_one, hasFDerivWithinAt_of_bilinear, mfderivWithin_projIcc_one, ContDiffMapSupportedIn.fderivCLM_apply_of_gt, TestFunction.fderivCLM_apply_of_le, ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, PointwiseConvergenceCLM.postcomp_apply, ContMDiffAt.mfderiv_apply, map_sub, exists_lt_apply_of_lt_opNNNorm, hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, le_opNorm, TestFunction.fderivCLM_ofSupportedIn, flipMultilinear_apply_apply, equivProdOfSurjectiveOfIsCompl_apply, SchwartzMap.integral_sesq_fourier_eq, MeasureTheory.aestronglyMeasurable_condExpL2, cfcL_integrable, adjointAux_norm, MeasureTheory.L1.setToL1_smul_left, ContinuousWithinAt.clm_apply_of_inCoordinates, MDifferentiable.clm_bundle_apply₂, fderiv, MeasureTheory.L1.setToL1_zero_left, ContinuousAffineMap.coe_mk_contLinear_eq_linear, EuclideanGeometry.orthogonalProjection_apply_mem, integrableAtFilter_comp, ProbabilityTheory.covarianceBilin_apply_basisFun_self, MeasureTheory.condExpInd_nonneg, hasStrictFDerivAt_of_bilinear, fpowerSeries_apply_zero, VectorPrebundle.mk_contMDiffCoordChange, mul_apply, VectorFourier.fourierIntegral_continuousLinearMap_apply, IsInvertible.bijective, norm_iteratedFDerivWithin_comp_left, ContinuousLinearEquiv.coeFn_ofBijective, integral_comp_comm', Pi.compRightL_apply, comp_memLp', map_smul_of_tower, SchwartzMap.fourier_lineDerivOp_eq, LinearMap.toContinuousBilinearMap_apply, ContinuousLinearMapWOT.inducingFn_apply, norm_iteratedFDerivWithin_clm_apply_const, RCLike.iInter_countable_halfSpaces_eq, ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith, CStarMatrix.inner_toCLM_conjTranspose_left, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, ContinuousAlgHom.coe_toContinuousLinearMap, pi_apply, TemperedDistribution.fourierInv_lineDerivOp_eq, MeasureTheory.condExpL2_indicator_ae_eq_smul, exists_lt_apply_of_lt_opNorm, mfderivWithin_comp_projIcc_one, IsMIntegralCurveOn.hasDerivWithinAt, Bundle.Trivialization.coe_continuousLinearEquivAt_eq, InnerProductSpace.toDualMap_apply_apply, PositiveLinearMap.leftMulMapPreGNS_apply, MeasureTheory.condExpL1CLM_of_aestronglyMeasurable', integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable, InnerProductSpace.HarmonicOnNhd.comp_CLM, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, UnitAddTorus.mFourierCoeff_toLp, ProbabilityTheory.gaussianReal_map_continuousLinearMap, Manifold.pathELength_def, mulLeftRight_apply, fromTangentSpace_mfderiv_smul_apply, Bundle.ContinuousRiemannianMetric.symm, analyticOn_bilinear, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left', InnerProductSpace.unique_continuousLinearMapOfBilin, deriv, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, MDifferentiable.clm_bundle_apply, coe_innerSL_apply, isCompact_image_coe_closedBall, RegularNormedAlgebra.isometry_mul', isClosed_image_coe_closedBall, DoubleCentralizer.central, coe_neg', MeasureTheory.integral_condExpL2_eq, IsCovariantDerivativeOn.torsion_self, VectorBundleCore.localTriv_symm_fst, MDifferentiableWithinAt.clm_bundle_apply₂, TestFunction.limitCLM_apply, hasFDerivAtFilter_iff_isLittleO, HasFDerivAt.clm_apply, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, hasDerivAt, antilipschitz_of_isEmbedding, hasFDerivAt_ringInverse, MeasureTheory.convolution_precompR_apply, WeakDual.coe_toStrongDual, NormedSpace.eq_zero_iff_forall_dual_eq_zero, SchwartzMap.compSubConstCLM_apply, ContinuousCohomology.I_obj_ρ_apply, MeasureTheory.setIntegral_condExpL2_indicator, InnerProductSpace.nnnorm_rankOne, OrthonormalBasis.orthogonalProjection_apply_eq_sum, ContinuousLinearEquiv.arrowCongr_apply, range_toLinearMap, coe_equivRange, setIntegral_compLp, VectorField.fderivWithin_pullbackWithin, toUniformConvergenceCLM_apply, interior_preimage, ContinuousAlternatingMap.curryLeft_apply_apply, contDiffPointwiseHolderAt, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, geometric_hahn_banach_of_nonempty_interior_point, SeparationQuotient.outCLM_uniformContinuous, InnerProductSpace.isSymmetricProjection_rankOne_self, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, Module.Basis.constrL_apply, MeasureTheory.L1.setToL1_mono_left', ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, MeasureTheory.ConvolutionExistsAt.integrable_swap, SchwartzMap.laplacianCLM_eq', VectorBundleCore.trivializationAt_coordChange_eq, apply_norm_sq_eq_inner_adjoint_left, measurable_apply₂, DifferentiableAt.fderiv_norm_self, ContDiff.continuous_fderiv_apply, fderivWithin_continuousAlternatingMap_apply_const_apply, const_apply_apply, ContinuousAt.clm_apply, EuclideanGeometry.orthogonalProjection_apply', GeneralSchauderBasis.expansion, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, uniformContinuous, proj_apply, ContinuousAffineMap.decompLinearIsometryEquiv_symm_apply, fderiv_of_bilinear, has_fderiv_at_filter_real_equiv, coe_mul', MeasureTheory.setIntegral_condExpInd, iteratedFDerivWithin_succ_apply_right, tendsto_integral_exp_smul_cocompact, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, SchwartzMap.toBoundedContinuousFunctionCLM_apply, extDeriv_apply_vectorField, ContDiffMapSupportedIn.monoCLM_eq_of_scalars, curveIntegral_segment, TestFunction.postcompCLM_apply, CovariantDerivative.torsion_apply, Real.fourierIntegral_continuousLinearMap_apply, IsCovariantDerivativeOn.torsion_antisymm, opNorm_mul_apply, norm_smulRightL, NormedSpace.inclusionInDoubleDualWeak_apply_apply, isBigO_id, MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable, AnalyticOn.compContinuousLinearMap, hasStrictFDerivAt_iff_isLittleO, MeasureTheory.convolution_def, MeasureTheory.norm_condExpL2_coe_le, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, compContinuousMultilinearMapL_apply, InnerProductSpace.trace_rankOne, exists_approx_preimage_norm_le, MeasureTheory.L1.setToL1_nonneg, isClosed_image_coe_of_bounded_of_weak_closed, NormedSpace.eq_iff_forall_dual_eq, summable, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, hasFDerivAt_norm_rpow, compL_apply, lsmul_flip_inj, MeasureTheory.Measure.addHaar_preimage_continuousLinearMap, analyticAt, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, RKHS.kerFun_apply, inCoordinates_apply_eq₂, FourierTransform.fourierInvCLM_apply, MeasureTheory.L1.integral_def, flip_apply, hasFDerivAt_iff_isLittleO, tangentMapWithin_snd, Matrix.toEuclideanCLM_toLp, ContinuousCohomology.Iobj_ρ_apply, ContinuousAt.clm_apply_of_inCoordinates, HasFDerivAt.comp_hasDerivAt, contDiffOn_stereoToFun, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, fderiv_inverse, BoundedContinuousFunction.toLp_inj, ContinuousMultilinearMap.restrictScalarsLinear_apply, ImplicitFunctionData.leftDeriv_fderiv_implicitFunction, toSpanSingleton_apply_map_one, HilbertBasis.hasSum_orthogonalProjection, bilinearRestrictScalars_apply_apply, InnerProductSpace.adjoint_rankOne, compFormalMultilinearSeries_apply', InnerProductSpace.rankOne_eq_zero, lipschitz, Real.fourierIntegral_convergent_iff', fderivWithin_continuousMultilinear_apply_const_apply, ContinuousAffineMap.coe_linear_eq_coe_contLinear, BoundedContinuousFunction.toLp_injective, Submodule.norm_sq_eq_add_norm_sq_starProjection, Bundle.ContMDiffRiemannianMetric.symm, InnerProductSpace.inner_right_rankOne_apply, VectorField.fderiv_pullback, SchwartzMap.pairing_apply, mfderivWithin_extChartAt_symm_inverse_apply, fderivWithin_comp_derivWithin, ContinuousAlternatingMap.apply_apply, HasFPowerSeriesWithinOnBall.unshift, innerSL_inj, fderivWithin_inv', MeasureTheory.lintegral_nnnorm_condExpL2_le, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, StrongDual.toLp_of_not_memLp, eqOn_closure_span, fderivWithin_of_bilinear, HasFPowerSeriesOnBall.compContinuousLinearMap, MeasureTheory.L1.setToFun_eq_setToL1, GeneralSchauderBasis.proj_apply_basis_mem, SeparationQuotient.outCLM_isUniformEmbedding, ContinuousMultilinearMap.ofSubsingleton_symm_apply_apply, curveIntegral_segment_const, 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, InnerProductSpace.rankOne_eq_rankOne_iff_comm, InnerProductSpace.toDual_apply, toContinuousAddMonoidHom_zero, leftInverse_of_comp, norm_map_of_mem_unitary, derivWithin, analyticWithinAt_uncurry_of_multilinear, precompR_apply, HarmonicAt.differentiableAt_complex_partial, integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, hasFDerivWithinAt_iff_isLittleO, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd', homeomorphOfUnit_apply, ProbabilityTheory.IsGaussian.charFun_eq', ProbabilityTheory.covarianceBilinDual_eq_covariance, MeasureTheory.condExpL1CLM_indicatorConstLp, SchwartzMap.postcompCLM_apply, ratio_le_opNorm, EuclideanSpace.coe_proj, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, HasStrictFDerivAt.isLittleO, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, ContDiffMapSupportedIn.structureMapCLM_zero_apply, TrivSqZeroExt.sndCLM_apply, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ContinuousAlternatingMap.curryLeft_compContinuousAlternatingMap, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, MeasureTheory.L1.setToL1_add_left', Submodule.norm_orthogonalProjection_apply_le, coe_pow', InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, ContMDiffAt.clm_apply_of_inCoordinates, InnerProductSpace.toDualMap_apply, geometric_hahn_banach_point_closed, MeasureTheory.L1.setToL1_mono_left, adjoint_inner_left, hasStrictDerivAt_of_bilinear, Continuous.clm_bundle_apply, isBoundedBilinearMap, apply_norm_eq_sqrt_inner_adjoint_right, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le, instContinuousEvalConst, VectorField.lieBracketWithin_smul_left, continuousMultilinearCurryRightEquiv_symm_apply, TemperedDistribution.fourierMultiplierCLM_apply, SchwartzMap.lineDeriv_eq_fourierMultiplierCLM, hasSum, lipschitz_apply, IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real, lsmul_apply, extDerivWithin_apply_vectorField_of_pairwise_commute, Bundle.ContMDiffRiemannianMetric.pos, equivRange_symm_apply, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, toContinuousAddMonoidHom_comp, IsContMDiffRiemannianBundle.exists_contMDiff, iteratedFDerivWithin_comp_left, InnerProductSpace.rank_rankOne, RCLike.geometric_hahn_banach_of_nonempty_interior', HasRightInverse.rightInverse_rightInverse, ContMDiffAt.clm_bundle_apply, Convex.taylor_approx_two_segment, InnerProductSpace.toDual_apply_apply, adjointAux_apply, inner_map_map_iff_adjoint_comp_self, ProbabilityTheory.IsGaussianProcess.comp_left, ContinuousMap.evalCLM_apply, ProperCone.innerDual_singleton, ContDiffWithinAt.continuousLinearMap_comp, Continuous.clm_apply, RKHS.kerFun_dense, InnerProductSpace.rankOne_def, IsLocalMinOn.hasFDerivWithinAt_nonneg, MDifferentiableAt.clm_bundle_apply₂, stereoToFun_apply, adjointAux_inner_left, coe_coe, SchwartzMap.convolution_apply, Submodule.sub_starProjection_mem_orthogonal, ConvexOn.real_univ_sSup_of_countable_affine_eq, add_apply, ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, HasSum.mapL, coe_projKerOfRightInverse_apply, ProbabilityTheory.covarianceBilin_comm, ContinuousMap.toLp_def, VectorField.lieBracket_fmul_left, SchwartzMap.integral_bilin_fourier_eq, HasFDerivWithinAt.lim, ContDiffMapSupportedIn.monoCLM_apply, ClosedSubmodule.orthogonal_eq_inter, hasFDerivWithinAt_iff_hasDerivWithinAt, ProperCone.coe_comap, ContinuousOn.clm_bundle_apply₂, NonUnitalAlgHom.coe_Lmul, ContinuousMultilinearMap.norm_map_init_le, iteratedFDerivWithin_comp_right, SchwartzMap.compCLMOfAntilipschitz_apply, SchwartzMap.fourierInv_apply_eq, SchwartzMap.smulRightCLM_apply_apply, hasStrictFDerivAt_iff_hasStrictDerivAt, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin, MeasureTheory.L1.setToL1_smul_left', VectorField.mpullback_apply, LinearMap.IsSymmetric.toSelfAdjoint_apply, VectorField.lieBracket_eq, SchwartzMap.toTemperedDistributionCLM_apply_apply, coe_restrict_scalarsL', DoubleCentralizer.star_fst, RCLike.geometric_hahn_banach_point_point, TestFunction.coe_ofSupportedInLM, Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable, SchauderBasis.proj_apply, Bundle.Trivialization.continuousLinearMapAt_symmL, iteratedFDerivWithin_one_apply, hasFiniteFPowerSeriesOnBall, IsCoercive.bounded_below, SchwartzMap.postcompCLM_postcompCLM, norm_iteratedFDeriv_le_of_bilinear, map_tsum, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, aestronglyMeasurable_comp₂, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left, IsLocalMinOn.hasFDerivWithinAt_eq_zero, MeasureTheory.setToFun_indicator_const, ContinuousMapZero.toContinuousMapCLM_apply, IsStarNormal.adjoint_apply_eq_zero_iff, ProperCone.hyperplane_separation_point, LinearEquiv.extendOfIsometry_symm_apply, Submodule.norm_sq_eq_add_norm_sq_projection, tangentCoordChange_comp, Matrix.inner_toEuclideanCLM, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, hasFDerivAtFilter, Submodule.starProjection_apply, hasFPowerSeriesOnBall_bilinear, eventually_nhds_zero_mapsTo, LineDeriv.laplacianCLM_eq_sum, MeasureTheory.norm_condExpInd_apply_le, LineDeriv.iteratedLineDerivOpCLM_apply, fromTangentSpace_mfderiv_smul_apply', Convex.isLittleO_alternate_sum_square, ContinuousAffineMap.decompEquiv_symm_apply, hasFDerivAt_iff_tendsto, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, deriv_of_bilinear, Orientation.areaForm'_apply, VectorBundleCore.coe_coordChange, hasFDerivAtFilter_iff_hasDerivAtFilter, innerSLFlip_apply_apply, isClosed_range_iff_antilipschitz_of_injective, Distribution.mapCLM_apply, ProbabilityTheory.HasIndepIncrements.map, bilinear_hasTemperateGrowth, IsContinuousRiemannianBundle.exists_continuous, ConvexOn.sSup_of_nat_affine_eq, postcomp_apply, Submodule.fst_orthogonalDecomposition_apply, prodMapL_apply, uncurryLeft_apply, Bundle.Trivialization.symmL_continuousLinearMapAt, antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range, Submodule.smul_starProjection_singleton, map_smulₛₗ, ContinuousAlternatingMap.curryLeft_compContinuousLinearMap, IsBilinearMap.toContinuousBilinearMap_apply, MDifferentiableWithinAt.clm_apply_of_inCoordinates, TestFunction.lineDerivOp_eq_lineDerivCLM, Complex.ofRealCLM_apply, InnerProductSpace.enorm_rankOne, differentiableAt_complex_iff_differentiableAt_real, mfderiv_coe_sphere_injective, cfcHom_real_eq_restrict, toLinearMap_innerSL_apply, SchwartzMap.fourierMultiplierCLM_apply, SchwartzMap.pderivCLM_apply, continuousMultilinearMapOption_apply_eq_self, ContinuousMultilinearMap.apply_apply, ContinuousMultilinearMap.flipLinear_apply_apply, WeakDual.CharacterSpace.coe_toCLM, comp_hasFPowerSeriesWithinOnBall, RKHS.inner_kerFun, CStarMatrix.toCLM_apply_single, lipschitzWith_of_opNorm_le, Submodule.inner_orthogonalProjection_eq_of_mem_right, IsSelfAdjoint.spectrumRestricts, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, HasFDerivWithinAt.norm_sq, lp.singleContinuousLinearMap_apply, geometric_hahn_banach_of_nonempty_interior', ProbabilityTheory.HasGaussianLaw.map, ContinuousMultilinearMap.toContinuousLinearMap_apply, one_apply, uncurryBilinear_apply, mfderiv_eq, MeasureTheory.integral_posConvolution, SchwartzMap.fourierInv_lineDerivOp_eq, VectorFourier.integral_fourierIntegral_swap, NormedSpace.inclusionInDoubleDualWeak_apply, Bundle.RiemannianMetric.symm, cpolynomialAt_uncurry_of_multilinear, MDifferentiableOn.clm_bundle_apply, Unitization.norm_eq_sup, ContinuousWithinAt.clm_apply, ProbabilityTheory.isGaussian_map, Matrix.ofLp_toEuclideanCLM, coe_add', CStarMatrix.toCLM_apply_eq_sum, le_of_opNorm_le, Submodule.eq_starProjection_of_mem_of_inner_eq_zero, ContDiff.comp_continuousLinearMap, MeasureTheory.Measure.map_conv_continuousLinearMap, exists_dual_vector, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fourierCoeff_toLp, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply, MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst, ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.variance_continuousLinearMap_gaussianReal, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', le_opNorm_of_le, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, iteratedDeriv_vcomp_three, VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt, SeparatingDual.eq_zero_iff_forall_dual_eq_zero, RCLike.sqrt_map, iteratedFDerivWithin_two_apply', TopModuleCat.hom_id, NormedSpace.equicontinuous_TFAE, differentiable, Submodule.starProjection_map_apply, SpectrumRestricts.real_iff, TrivSqZeroExt.inrCLM_apply, continuousWithinAt_uncurry_of_multilinear, sSup_sphere_eq_norm, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, LinearPMap.adjointDomainMkCLM_apply, ContDiffPointwiseHolderAt.continuousLinearMap_comp, memLp_of_bilin, SchwartzMap.smulLeftCLM_smulLeftCLM_apply, VectorField.mlieBracketWithin_smul_left, iInter_halfSpaces_eq, isometry_iff_adjoint_comp_self, differentiableWithinAt, geometric_hahn_banach_closed_compact, HasFDerivWithinAt.mapsTo_tangent_cone, postcompCompactConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, ProbabilityTheory.covarianceBilin_self_nonneg, compLeftContinuous_apply, complexOfReal_deriv, ApproximatesLinearOn.lipschitz_sub, opNorm_mulLeftRight_apply_le, analyticOnNhd_bilinear, reApplyInnerSelf_apply, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', differentiableAt, sub_apply, ProbabilityTheory.covarianceBilinDual_self_eq_variance, LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply, SchauderBasis.RankOneDecomposition.basisCoeff_spec, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, geometric_hahn_banach_open_open, iteratedFDerivWithin_succ_apply_left, hasStrictFDerivAt_norm_sq, Submodule.starProjection_unit_singleton, SchwartzMap.fourier_evalCLM_eq, ContinuousLinearEquiv.equivOfInverse_apply, LinearMap.compLeftInverse_apply_of_bdd, ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, map_sub₂, QuasispectrumRestricts.real_iff, bilinearComp_apply, LinearEquiv.extendOfIsometry_apply, SchwartzMap.evalCLM_apply_apply, OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective, ContMDiffWithinAt.clm_bundle_apply₂, toContinuousLinearEquivOfDetNeZero_apply, tendsto_integral_exp_smul_cocompact_of_inner_product, ContinuousMultilinearMap.compContinuousLinearMap_apply, CStarMatrix.toCLM_apply, RKHS.coeCLM_injective, SeparationQuotient.mk_outCLM, norm_map_tail_le, ContinuousAffineMap.map_vadd, VectorField.mlieBracketWithin_smul_right, compContinuousAlternatingMap_coe, compContinuousMultilinearMap_coe, exists_dual_vector'', FormalMultilinearSeries.compContinuousLinearMap_applyComposition, MeasureTheory.MemLp.continuousLinearMap_comp, ProbabilityTheory.IsGaussian.memLp_dual, TestFunction.lineDerivCLM_eq_fderivCLM, ProbabilityTheory.covarianceBilinDual_self_nonneg, conformalFactorAt_inner_eq_mul_inner', ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply, ProbabilityTheory.isGaussian_map_of_measurable, TemperedDistribution.fourier_lineDerivOp_eq, ContDiffPointwiseHolderAt.clm_apply, MeasureTheory.charFunDual_map_const_add, MeasureTheory.L1.SimpleFunc.setToL1S_const, MeasureTheory.charFunDual_map_add_const, LinearMap.extendOfNorm_eq, integrable_comp, adjointAux_adjointAux, TopModuleCat.freeMap_map, Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl, MeasureTheory.condExpL2_indicator_of_measurable, TestFunction.lineDerivCLM_apply, ProbabilityTheory.covarianceBilin_real_self, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, ContDiffOn.continuousOn_fderivWithin_apply, MeasureTheory.condExp_ae_eq_condExpL1CLM, LinearEquiv.extend_symm_apply, integral_comp_id_comm', coprodEquivL_apply_apply, BoundedContinuousFunction.coeFn_toLp, isBigOWith_comp, continuous_clm_apply, ContinuousLinearEquiv.skewProd_apply, hasTemperateGrowth, VectorFourier.fourierSMulRight_apply, measurable_fderiv_apply_const, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, toContinuousAddMonoidHom_injective, InnerProductSpace.gramSchmidt_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, VectorBundleCore.localTriv_coordChange_eq, ContinuousMultilinearMap.uncurryRight_apply, MeasureTheory.L1.tendsto_setToL1, isVonNBounded_iff, MeasureTheory.condExpL1CLM_indicatorConst, SchwartzMap.fourierMultiplierCLM_ofReal, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, ContDiffWithinAt.comp_continuousLinearMap, ContDiffWithinAt.laplacianWithin_CLM_comp_left, Manifold.riemannianEDist_def, HasFDerivAtFilter.isLittleO, range_coeFn_eq, isVonNBounded_image2_apply, MeasureTheory.weightedSMul_smul, MeasureTheory.integral_continuousLinearMap_prod, NonlinearRightInverse.right_inv, curveIntegralFun_def', integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2, norm_extendTo𝕜'_bound, HasFDerivWithinAt.hasDerivWithinAt, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, HasGradientWithinAt.fderivWithin_apply, ContMDiffOn.clm_apply, MeasureTheory.L1.setToL1_unique, cfc_eq_cfcL_mkD, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, contDiff_succ_iff_fderiv_apply, VectorBundleCore.localTriv_apply, LinearIsometryEquiv.coe_coe'', NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, ContinuousAffineMap.decompAffineEquiv_symm_apply, RKHS.coeCLM_apply, IsPositive.re_inner_nonneg_left, ProbabilityTheory.HasGaussianLaw.map_of_measurable, extDerivWithin_apply_vectorField, measurable_comp, Real.fourier_bilin_convolution_eq, BoxIntegral.BoxAdditiveMap.toSMul_apply, ProbabilityTheory.IsGaussian.map_rotation_eq_self, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, hasFDerivWithinAt, IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt, CStarMatrix.mul_entry_mul_eq_inner_toCLM, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, le_opNorm₂, lpPairing_eq_integral, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, norm_iteratedFDeriv_comp_left, LinearMap.clmOfExistsBoundedImage_apply, ProbabilityTheory.covarianceOperator_inner, InnerProductSpace.rankOne_def', ContDiff.fderiv_apply, HasFDerivAt.comp_hasDerivWithinAt, fderiv_apply_one_eq_deriv, MDifferentiableAt.clm_apply_of_inCoordinates, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, HasFTaylorSeriesUpToOn.compContinuousLinearMap, SchwartzMap.integral_sesq_fourierIntegral_eq, Submodule.norm_orthogonalProjection_apply, IsPositive.inner_nonneg_left, map_add, apply_norm_eq_sqrt_inner_adjoint_left, TestFunction.monoCLM_eq_of_scalars, coe_copy, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left', fderiv_continuousMultilinear_apply_const_apply, MeasureTheory.Integrable.convolution_integrand, MeasureTheory.condExpL1CLM_lpMeas, ProbabilityTheory.HasGaussianLaw.map_fun, ContMDiffWithinAt.clm_bundle_apply, Submodule.eq_starProjection_of_mem_orthogonal, Differentiable.clm_apply, mdifferentiableWithinAt, ContMDiff.clm_bundle_apply, ProbabilityTheory.covarianceBilin_apply_pi, SchwartzMap.integral_bilinear_laplacian_right_eq_left, natCast_apply, HasFDerivAt.lim, isometry_mul, antilipschitz_of_injective_of_isClosed_range, ProbabilityTheory.integral_strongDual_stdGaussian, isOpen_injective, StrongDual.toLpₗ_apply, MeasureTheory.L1.setToL1_apply_coeToLp, HasStrictFDerivAt.isEquivalent_sub, continuous_uncurry_of_multilinear, LinearIsometry.map_starProjection, inr_apply, MeasureTheory.dist_convolution_le', ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, CovariantDerivative.torsion_eq_zero_iff, MeasureTheory.integral_continuousLinearMap_prod', ConvexOn.real_univ_sSup_affine_eq, toSpanSingleton_one, SchauderBasis.proj_comp, ContMDiff.clm_bundle_apply₂, MeasureTheory.L1.setToL1_congr_left', measurable_apply, hasFDerivAtFilter_iff_isLittleOTVS, second_derivative_symmetric, ContinuousAlternatingMap.curryLeft_same, ContinuousMultilinearMap.curryRight_apply, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, Distribution.dsupport_smulLeftCLM_subset, Submodule.inner_orthogonalProjection_eq_of_mem_left, sSup_unit_ball_eq_nnnorm, extendTo𝕜_apply, MeasureTheory.SimpleFunc.setToSimpleFunc_indicator, HasFDerivAt.comp_hasDerivWithinAt_of_eq, ProbabilityTheory.IsGaussian.integral_dual, ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds, VectorPrebundle.exists_coordChange, continuous, MDifferentiableOn.clm_apply, MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral, ContDiffMapSupportedIn.postcompCLM_apply, SchwartzMap.compSubConstCLM_comp, IsContDiffImplicitAt.bijective, Submodule.eq_starProjection_of_mem_orthogonal', ProbabilityTheory.covarianceBilin_apply_basisFun, coe_piMap', ContinuousMultilinearMap.analyticOn_uncurry_of_linear, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, algebraMapCLM_apply, iteratedFDeriv_one_apply, ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft, HasFDerivAt.hasLineDerivAt, MeasureTheory.L1.setToL1_congr_left, adjoint_comp_self_injective_iff, iteratedFDeriv_succ_apply_right, hasMFDerivAt, ProbabilityTheory.variance_dual_stdGaussian, TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, ContDiffMapSupportedIn.fderivCLM_eq_of_scalars, fderiv_deriv, MeasureTheory.L1.setToL1_smul, ContinuousLinearEquiv.coe_apply, HasFDerivAt.lim_real, PointwiseConvergenceCLM.precomp_apply, ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, toContinuousAddMonoidHom_inj, analyticOnNhd_uncurry_of_multilinear, InnerProductSpace.isStarProjection_rankOne_self, SeparationQuotient.mk_comp_outCLM, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, ContinuousLinearMapWOT.ext_dual_iff, contDiff_clm_apply_iff, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, hasStrictFDerivAt, oneTangentSpaceIcc_def, TrivSqZeroExt.inlCLM_apply, hasFPowerSeriesAt_bilinear, comp_analyticOn, self_comp_adjoint_injective_iff, Bundle.Trivialization.continuousLinearMapAt_apply, coeFn_compLpL, Real.Lp.fourierTransformCLM_apply, sub_apply', coeFn_injective, contDiffOn_clm_apply, le_opNNNorm, Bundle.Trivialization.symmL_apply, fderiv_continuousAlternatingMap_apply_apply, PiTensorProduct.mapLMultilinear_apply_apply, HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq, HasFDerivWithinAt.clm_comp, uncurryMid_apply, evalL_apply, isBoundedBilinearMap_apply, AEMeasurable.apply_continuousLinearMap, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left', integral_comp_commSL, Complex.sqrt_map, hasStrictFDerivAt_ringInverse, mul_apply', ContDiffOn.continuousLinearMap_comp, Unitary.norm_map, Submodule.starProjection_apply_mem, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, InnerProductSpace.rankOne_comp_rankOne, geometric_hahn_banach_point_open, TestFunction.mkCLM_apply, SchauderBasis.proj_apply_basis_mem, BoxIntegral.hasIntegral_const, ContinuousMap.toLp_injective, TestFunction.fderivCLM_eq_of_scalars, DifferentiableAt.comp_semilinear₁, ContinuousAlternatingMap.compContinuousLinearMap_apply, PiTensorProduct.mapL_apply, MeasureTheory.integrable_continuousLinearMap_prod', TestFunction.lineDerivCLM_eq_of_scalars, ContinuousMapZero.evalCLM_apply, isCompactOperator_of_locallyCompactSpace_rng, InnerProductSpace.rankOne_comp, StrongDual.mem_polarSubmodule, exists_dual_vector', MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, SchwartzMap.tsupport_smulLeftCLM_subset, InnerProductSpace.toMatrix_rankOne, separate_convex_open_set, cfcₙHom_real_eq_restrict, opNorm_le_iff, RCLike.geometric_hahn_banach_open, completion_apply_coe, InnerProductSpace.isSymmetric_rankOne_self, ContinuousMap.coe_toLp, continuousMultilinearCurryLeftEquiv_apply, PolynormableSpace.banach_steinhaus, ContinuousAlternatingMap.ofSubsingleton_apply_apply, precomp_compactConvergenceCLM_apply, unitary.norm_map, ContinuousAlternatingMap.restrictScalarsCLM_apply, ContMDiffWithinAt.mfderivWithin_apply, SchwartzMap.tsupport_fderivCLM_subset, isBigOTVS_comp, NonlinearRightInverse.right_inv', integral_comp_L1_comm, intervalIntegral_apply, selfAdjointPartL_apply_coe, HasFDerivWithinAt.comp_hasDerivWithinAt, HasFDerivWithinAt.isEquivalent_sub, fderivWithin_continuousAlternatingMap_apply_apply, toContinuousAddMonoidHom_neg, norm_iteratedFDerivWithin_le_of_bilinear, MeasureTheory.aestronglyMeasurable_condExpL1CLM, ofNat_apply, ContDiffMapSupportedIn.seminorm_apply, GeneralSchauderBasis.ortho, VectorField.lieBracket_smul_left, rotation_apply, coe_sum', SchwartzMap.convolution_continuous_left, adjoint_toSpanSingleton, ext_iff, ContDiffMapSupportedIn.structureMapCLM_top_apply, mfderivWithin_eq, IsExposed.eq_inter_halfSpace, continuousOn_uncurry_of_multilinear, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, MeasureTheory.integrable_condExpL2_indicator, tangentCoordChange_self, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, spectrum.hasFDerivAt_resolvent, exists_mul_lt_apply_of_lt_opNNNorm, RKHS.kerFun_inner, IsBoundedBilinearMap.toContinuousLinearMap_apply, AlgHom.coe_toContinuousLinearMap, SchwartzMap.pairing_continuous_left, ConvexOn.univ_sSup_affine_eq, smulRight_comp_smulRight, SchwartzMap.integralCLM_apply, IsCovariantDerivativeOn.add_one_form, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair, HasStrictFDerivAt.hasStrictDerivAt, hasFDerivAt_iff_isLittleOTVS, ConvexOn.real_univ_sSup_of_nat_affine_eq, projKerOfRightInverse_comp_inv, neg_apply, innerSLFlip_apply, ContinuousAt.clm_bundle_apply₂, fderivWithin_derivWithin, toContinuousAddMonoidHom_restrictScalars, ProbabilityTheory.covarianceBilin_real, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', TopModuleCat.forget₂_TopCat_obj, measurable_coe, analyticOn, nndist_le_opNNNorm, SchwartzMap.lineDerivOp_fourierInv_eq, opNorm_mulLeftRight_apply_apply_le, VectorPrebundle.mk_coordChange, ConvexOn.real_sSup_of_countable_affine_eq, cfcL_integral, ContinuousMap.coeFn_toLp, MeasureTheory.L1.norm_setToL1_le_mul_norm', homeomorphOfUnit_symm_apply, innerSL_apply_norm, Real.fourier_bilin_convolution_eq_integral, SeparationQuotient.liftCLM_apply, SchauderBasis.RankOneDecomposition.exists_coeff, ContinuousWithinAt.clm_bundle_apply₂, fderivWithin, Submodule.subtypeL_apply, ContinuousAffineMap.coe_contLinear, curveIntegral_eq_intervalIntegral_deriv, fderivWithin_clm_comp, ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars, continuousSemilinearMapClass, lp.tsumCLM_apply, ContDiffAt.continuousLinearMap_comp, ProbabilityTheory.variance_dual_prod', HasCompactSupport.fderiv_apply, SchauderBasis.succSub_ortho, ProbabilityTheory.covarianceBilinDual_comm, ProbabilityTheory.isGaussian_iff_charFunDual_eq, NormedSpace.isEmbedding_inclusionInDoubleDualWeak, opNNNorm_mul_flip_apply, compLeftContinuousBounded_apply, CovariantDerivative.torsion_antisymm, Submodule.starProjection_orthogonalComplement_singleton_eq_zero, ContMDiffWithinAt.clm_apply_of_inCoordinates, ContinuousMultilinearMap.curryMid_apply, HasFDerivWithinAt.comp_hasDerivAt, SchwartzMap.compCLM_apply, TemperedDistribution.fourierMultiplierCLM_apply_apply, ContinuousMap.toLp_comp_toContinuousMap, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, hasFDerivAt_uncurry_of_multilinear, toContinuousAddMonoidHom_id, opNorm_mul_apply_le, smul_def, Submodule.lipschitzWith_starProjection, MDifferentiableWithinAt.clm_bundle_apply, isPositive_iff_complex, toContinuousAddMonoidHom_sub, ProbabilityTheory.covarianceBilin_apply, isThetaTVS_comp, BoxIntegral.integralSum_sub_partitions, comp_cpolynomialOn, HasFDerivAt.linear_multilinear_comp, IsBoundedBilinearMap.deriv_apply, TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, ContinuousLinearEquiv.skewProd_symm_apply, MeasureTheory.convolutionExistsAt_iff_integrable_swap, StronglyMeasurable.apply_continuousLinearMap, HasFDerivAt.hasDerivAt, isPositive_iff, TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, ContinuousMultilinearMap.compContinuousLinearMapL_apply, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, IsInvertible.inverse_apply_self, HasFDerivWithinAt.unique_on, VectorField.pullbackWithin_eq, nhds_zero_eq, PiTensorProduct.liftIsometry_apply_apply, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, ProbabilityTheory.covarianceBilin_map, Unitization.nnnorm_eq_sup, SchwartzMap.fourierTransformCLM_apply, skewAdjointPartL_apply_coe, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, MeasureTheory.Lp.constL_apply, SchwartzMap.fderivCLM_fourier_eq, HasFDerivWithinAt.isLittleOTVS, Bundle.ContinuousRiemannianMetric.pos, SchwartzMap.derivCLM_apply, RCLike.map_nonneg_iff, IsCoercive.continuousLinearEquivOfBilin_apply, LinearMap.toContinuousLinearMap₁_apply, projKerOfRightInverse_apply_idem, TemperedDistribution.fourierTransformCLM_apply, mfderiv_comp_apply, TopModuleCat.cokerπ_surjective, Unitary.inner_map_map, VectorField.lieBracketWithin_smul_right, isCompactOperator_of_tendsto, inner_gradientWithin_left, ContinuousAffineMap.decompLinearEquiv_symm_apply, tsupport_fderiv_apply_subset, isConformalMap_iff, ContDiff.clm_apply, VectorFourier.integral_bilin_fourierIntegral_eq_flip, deriv_clm_apply, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, ContinuousMultilinearMap.ofSubsingleton_apply_apply, IsInvertible.inverse_comp_apply_of_right, InnerProductSpace.toLinearMap_rankOne, comp_hasFPowerSeriesOnBall, coe_codRestrict_apply, adjointAux_inner_right, isCompact_closure_image_coe_of_bounded, VectorField.mpullback_mfderivWithin_apply_smul, Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real, Bundle.RiemannianMetric.pos, HasStrictFDerivAt.clm_apply, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, ContMDiffAt.clm_bundle_apply₂, continuousMultilinearCurryRightEquiv_symm_apply', MeasureTheory.condExpInd_smul', isBigO_sub, ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, LinearMap.norm_extendOfNorm_apply_le, MeasureTheory.L1.setToL1_add_left, antilipschitz_of_bound, Manifold.pathELength_eq_lintegral_mfderiv_Icc, IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn, TensorialAt.mkHom_apply, HasFDerivAtFilter.isLittleOTVS, ContinuousAffineMap.contLinear_map_vsub, LinearPMap.adjointDomainMkCLMExtend_apply, dimH_orthogonalProjection_le, iteratedFDerivWithin_two_apply, DoubleCentralizer.coe_fst, coprod_apply, coe_fst', HasLeftInverse.isClosed_range, Submodule.re_inner_starProjection_nonneg, OrthogonalFamily.sum_projection_of_mem_iSup, Real.fourierIntegral_continuousLinearMap_apply', TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, hasFDerivAt_of_bilinear, contDiffOn_succ_iff_fderiv_apply, StrongDual.extendRCLike_apply, OpenPartialHomeomorph.MDifferentiable.mfderiv_injective, LinearMap.toContPerfPair_apply, MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter, ContDiffMapSupportedIn.continuous_iff_comp_order_le, TensorialAt.mkHom₂_apply, TensorialAt.mkHom_apply_eq_extend, Submodule.starProjection_orthogonal_apply_eq_zero, VectorFourier.fourierPowSMulRight_apply, extDeriv_apply_vectorField_of_pairwise_commute, OrthonormalBasis.norm_dual, ContMDiffWithinAt.clm_apply, coe_restrictScalars', isBoundedLinearMap, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, opNorm_le_iff_lipschitz, SchwartzMap.convolution_flip, MeasureTheory.L1.norm_setToL1_le_mul_norm, IsLocalMaxOn.fderivWithin_eq_zero, MeasureTheory.charFunDual_dirac, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, precompCompactConvergenceCLM_apply, VectorField.mpullbackWithin_apply, coe_snd', StrongDual.toWeakDual_apply, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left', IsCompactOperator.comp_clm, SchwartzMap.lineDerivOp_apply_eq_fderiv, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub, conformalFactorAt_inner_eq_mul_inner, RKHS.kernel_inner, BoxIntegral.integral_const, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, differentiableOn, isPositive_iff', TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, ProperCone.mem_comap, ContinuousMultilinearMap.curryLeft_apply, ContDiffAt.laplacian_CLM_comp_left_nhds, Submodule.lipschitzWith_orthogonalProjection, norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, TopModuleCat.kerι_apply, MeasureTheory.Integrable.apply_continuousLinearMap, coe_prodMap', UniformSpace.Completion.coe_toComplL, ProperCone.hyperplane_separation_of_notMem, fderiv_clm_apply, ContinuousLinearEquiv.ofBijective_symm_apply_apply, TestFunction.monoCLM_apply, HasFPowerSeriesWithinAt.unshift, hasFDerivAtFilter_iff_tendsto, det_smulRight, innerSL_apply, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, tendsto_birkhoffAverage_orthogonalProjection, InnerProductSpace.isIdempotentElem_rankOne_self_iff, Submodule.norm_starProjection_apply, cfc_eq_cfcL, stereographic_apply, MeasureTheory.inner_condExpL2_eq_inner_fun, StrongDual.toLp_apply, map_smul₂, Submodule.inner_starProjection_left_eq_right, PiLp.proj_apply, WeakSpace.coe_map, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, IsConformalMap.injective, Continuous.clm_bundle_apply₂, MeasureTheory.condExpInd_disjoint_union_apply, analyticOn_uncurry_of_multilinear, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst, Bornology.IsVonNBounded.image, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left, exists_embedding_euclidean_of_compact, coe_id', Submodule.starProjection_minimal, contMDiffWithinAt, IsCovariantDerivativeOn.torsion_apply_eq_extend, Real.differentiable_fourierChar_neg_bilinear_right, OrthonormalBasis.sum_rankOne_eq_id, dslope_comp, inl_apply, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, Submodule.orthogonalProjection_orthogonal_apply_eq_zero, 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, adjoint_inner_right, exists_extension_norm_eq, DifferentiableWithinAt.clm_apply, SeparationQuotient.isEmbedding_outCLM, ContDiff.contDiff_fderiv_apply, measurable_apply', toSpanSingletonLE_symm_apply, MeasureTheory.condExp_bilin_of_stronglyMeasurable_right, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt, ContDiffMapSupportedIn.postcompLM_apply, CovariantDerivative.torsion_self, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, DifferentiableAt.clm_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, SchwartzMap.tsupport_derivCLM_subset, HasFDerivAt.comp_semilinear, MeasureTheory.integrable_continuousLinearMap_prod, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, ContDiffWithinAt.fderivWithin_right_apply, MeasureTheory.setToFun_const, StrongDual.im_extendRCLike_apply, MeasureTheory.charFunDual_map, le_of_opNorm₂_le_of_le, ofTendstoOfBoundedRange_apply, AddMonoidHom.coe_toRealLinearMap, Submodule.orthogonalProjectionFn_eq, iteratedFDerivWithin_clm_apply_const_apply, ContinuousAlternatingMap.toContinuousLinearMap_apply, signedDist_apply, continuousMultilinearCurryRightEquiv_apply', TemperedDistribution.lineDerivOp_fourierInv_eq, ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero, AnalyticAt.compContinuousLinearMap, ProbabilityTheory.variance_dual_prod, TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, isBigOTVS_fun_comp, SeparationQuotient.liftCLM_mk, coeFn_compLp, isOpenMap, ContDiffMapSupportedIn.fderivCLM_apply, RCLike.geometric_hahn_banach_of_nonempty_interior, MeasureTheory.L1.setToL1_mono, extendTo𝕜'_apply, TestFunction.fderivCLM_apply, isAdjointPair_inner, SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply, coe_sub', ProbabilityTheory.norm_uncenteredCovarianceBilin_le, complexOfReal_hasDerivAt, Real.hasFDerivAt_fourierChar_neg_bilinear_right, RCLike.re_extendTo𝕜ₗ, ContDiffMapSupportedIn.continuous_iff_comp, smulRight_comp, cfcₙ_eq_cfcₙL, ContDiffOn.comp_continuousLinearMap, VectorFourier.norm_fourierSMulRight, smulRight_one_one, LinearEquiv.extend_apply, hasStrictFDerivAt_inv', cfcₙL_apply, Submodule.snd_orthogonalDecomposition_apply, TemperedDistribution.smulLeftCLM_const, SchwartzMap.smulLeftCLM_apply_apply, MDifferentiable.clm_apply, SchwartzMap.fourier_fderivCLM_eq, integral_comp_id_comm, StrongDual.re_extendRCLike_apply, SchwartzMap.fourier_convolution_apply, MeasureTheory.SimpleFunc.setToSimpleFunc_const', iteratedFDeriv_two_apply, analyticOnNhd, IsLocalMaxOn.hasFDerivWithinAt_eq_zero, StrongDual.coe_toWeakDual, ContMDiffAt.clm_apply, WeakDual.toStrongDual_apply, hasMFDerivWithinAt, Real.differentiable_fourierChar_neg_bilinear_left, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, continuousMultilinearCurryLeftEquiv_symm_apply, LineDeriv.lineDerivOpCLM_apply, geometric_hahn_banach_closed_point, ContinuousMultilinearMap.smulRightL_apply, contDiff, Convex.second_derivative_within_at_symmetric_of_mem_interior, isUniformEmbedding_toUniformOnFun, exists_mul_lt_of_lt_opNorm, toWeakSpaceCLM_eq_toWeakSpace, IsLocalMinOn.fderivWithin_nonneg, Submodule.orthogonalDecomposition_apply, contMDiffOn, CovariantDerivative.torsion_apply_eq_extend, EuclideanSpace.restrict₂_apply, Convex.norm_image_sub_le_of_norm_fderiv_le', OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ, nnbound, RCLike.iInter_halfSpaces_eq', PointwiseConvergenceCLM.evalCLM_apply, topDualPairing_apply, isCompactOperator_of_locallyCompactSpace_dom, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left, ContDiffMapSupportedIn.structureMapCLM_zero_injective, RCLike.iInter_halfSpaces_eq, MeasureTheory.setIntegral_condExpL1CLM, ProperCone.hyperplane_separation, cpolynomialOn, coe_complexOfReal, le_opENorm, continuousMultilinearCurryFin1_symm_apply, MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound, StrongDual.mem_polar_iff, Submodule.orthogonal_eq_inter, mdifferentiableOn, MeasureTheory.eLpNorm_condExpL2_le, Complex.integral_boundary_rect_of_differentiableOn_real, lsmul_flip_apply, SchwartzMap.coe_apply, ContinuousLinearEquiv.coord_self, compContinuousAlternatingMapCLM_apply_apply, RCLike.geometric_hahn_banach_compact_closed, SchwartzMap.smulLeftCLM_ofReal, extDerivWithin_apply, ContinuousAt.clm_bundle_apply, sSup_unitClosedBall_eq_norm, iteratedDeriv_vcomp_two, fderiv_norm_rpow, norm_map_iff_adjoint_comp_self, MeasureTheory.L1.integral_eq', Submodule.starProjection_orthogonal_val, VectorField.lieBracketWithin_eq, ContinuousAlternatingMap.liftCLM_apply, RCLike.geometric_hahn_banach_point_closed, ContinuousLinearEquiv.coe_coe, SchauderBasis.RankOneDecomposition.proj_comp, map_add₂, MeasureTheory.integral_bilinear_hasDerivAt_eq_sub, VectorField.fderivWithin_apply_lieBracket, HasFPowerSeriesWithinAt.compContinuousLinearMap, VectorPrebundle.coordChange_apply, EuclideanGeometry.orthogonalProjection_apply, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono, hasDerivWithinAt, FormalMultilinearSeries.derivSeries_apply_diag, iteratedFDeriv_clm_apply_const_apply, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, IsExposed.eq_inter_halfSpace', ProbabilityTheory.covarianceBilinDual_of_not_memLp, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn, prod_apply, Complex.imCLM_apply, MeasureTheory.charFun_map_eq_charFunDual_smul, integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable, InnerProductSpace.continuousLinearMapOfBilin_apply, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NormedSpace.double_dual_bound, MeasureTheory.convolution_eq_swap, map_zero₂, VectorField.mlieBracketWithin_apply, SchwartzMap.smulLeftCLM_apply, ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, MeasureTheory.condExpIndSMul_ae_eq_smul, iteratedFDeriv_comp_right, HasFDerivAtFilter.isEquivalent_sub, ContDiff.continuousLinearMap_comp, precomp_apply, hasFDerivWithinAt_iff_isLittleOTVS, cfcₙL_integrable, HasGradientAt.fderiv_apply, differentiableWithinAt_complex_iff_differentiableWithinAt_real, comp_analyticOnNhd, TemperedDistribution.derivCLM_apply_apply, MeasureTheory.L1.setToL1'_eq_setToL1SCLM, locallyIntegrableOn_comp, precomp_uniformConvergenceCLM_apply, mfderiv_subtype_coe_Icc_one, exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm, coe_pi', postcompUniformConvergenceCLM_apply, VectorField.lieBracket_smul_right, coeFn_ofSeqClosedGraph, InnerProductSpace.HarmonicAt.comp_CLM, isHomeomorph_of_isUnit, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound, smulRight_apply, analyticAt_bilinear, inner_gradient_left, FormalMultilinearSeries.compContinuousLinearMap_apply, ConvexOn.exists_affine_le_of_lt, ProbabilityTheory.IsGaussian.charFunDual_eq', HasFDerivWithinAt.comp_hasDerivAt_of_eq, contDiffOn_fderivWithin_apply, toPointwiseConvergenceCLM_apply, apply_norm_sq_eq_inner_adjoint_right, IsCovariantDerivativeOn.torsion_apply, innerSL_apply_coe, bound, StrongDual.polar_singleton, MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg, toUniformConvergenceCLM_symm_apply, MeasureTheory.ContinuousMap.inner_toLp, ConvexOn.real_sSup_of_nat_affine_eq, integral_bilinear_fderiv_right_eq_neg_left_of_integrable, hasFDerivAt_inv', coe_mk', DifferentiableAt.comp_semilinear₂, exists_continuousLinearEquiv_fderiv_symm_eq, TensorialAt.mkHom₂_apply_eq_extend, MeasureTheory.AEStronglyMeasurable.convolution_integrand', map_neg, IsInvertible.self_apply_inverse, isOpenMap_of_ne_zero, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, integral_comp_comm, hasFDerivWithinAt_iff_tendsto, map_neg₂, coe_toContinuousAffineMap, Bundle.RiemannianMetric.continuousAt, ContinuousLinearMapWOT.continuous_dual_apply, iteratedFDeriv_comp_left, isCompact_image_coe_of_bounded_of_weak_closed, Submodule.orthogonalProjection_eq_zero_iff, holderL_apply_apply, StrongDual.mem_polar_singleton, HasFDerivAt.isEquivalent_sub, ContMDiffOn.clm_bundle_apply, MeasureTheory.condExpL1CLM_smul, MeasureTheory.AEStronglyMeasurable.convolution_integrand, VectorFourier.hasFDerivAt_fourierChar_smul, IsInvertible.injective, Submodule.orthogonalProjection_starProjection_of_le, GeneralSchauderBasis.proj_comp, Real.exists_extension_norm_eq, continuousMultilinearCurryRightEquiv_apply, integrableOn_comp, Submodule.coe_orthogonalProjection_apply, integrable_of_bilin_of_bdd_right, intrinsicStar_apply, SeparationQuotient.mkCLM_apply, fderiv_comp_deriv_of_eq, extend_eq, apply_apply', ProbabilityTheory.covarianceBilinDual_of_not_memLp', Submodule.starProjection_apply_eq_zero_iff, SchwartzMap.fourier_convolution, AnalyticOnNhd.eval_continuousLinearMap', apply_val_ker, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, HasFPowerSeriesAt.compContinuousLinearMap, ImplicitFunctionData.rightDeriv_fderiv_implicitFunction, fderivWithin_clm_apply, postcomp_uniformConvergenceCLM_apply, exists_continuousLinearEquiv_fderivWithin_symm_eq, instLocallyBoundedMapClass, bijective_iff_dense_range_and_antilipschitz, dist_le_opNorm, FourierTransform.fourierCLM_apply, fderiv_continuousAlternatingMap_apply_const_apply, InnerProductGeometry.IsConformalMap.preserves_angle, complexOfReal_derivWithin, ApproximatesLinearOn.lipschitzOnWith, isBigOTVS_id, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure, ClosedSubmodule.coe_comap, hasStrictDerivAt, analyticAt_uncurry_of_multilinear, measurable_fderiv_apply_const_with_param, ContinuousLinearEquiv.fst_equivOfRightInverse, bound_of_antilipschitz, HasStrictFDerivAt.clm_comp, WithLp.fstL_apply, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, MeasureTheory.L1.integral_eq, smulRightL_apply_apply, continuousOn_clm_apply, toSpanSingletonCLE_apply_apply, ContinuousAlternatingMap.compContinuousLinearMapCLM_apply, IsInvertible.inverse_comp_apply_of_left, opNNNorm_mul_apply, fderivInnerCLM_apply, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, TestFunction.injective_toBoundedContinuousFunctionCLM, ConvexOn.sSup_affine_eq, VectorBundleCore.coordChange_comp, MeasureTheory.L1.setToL1'_apply_coeToLp, SchwartzMap.denseRange_toLpCLM, SchwartzMap.toZeroAtInftyCLM_apply, toSpanSingletonCLE_symm_apply, Real.fderiv_fourierChar_neg_bilinear_left_apply, apply_apply, MeasureTheory.L1.setToL1_const, norm_map_removeNth_le, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply, IsSymmSndFDerivWithinAt.eq, map_smulₛₗ₂, fderivWithin_restrictScalars_comp, RCLike.geometric_hahn_banach_closed_compact, ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto, ContinuousOn.clm_bundle_apply, inner_gradient_right, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, derivWithin_clm_apply, Submodule.orthogonalProjection_orthogonal, MeasureTheory.L1.setToL1_lipschitz, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd, TemperedDistribution.fourierTransformInvCLM_apply, MDifferentiableWithinAt.clm_apply, HasCompactSupport.convolution_integrand_bound_right, 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, AnalyticOnNhd.eval_continuousLinearMap, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero, HasFDerivAt.clm_comp, adjoint_innerSL_apply, hasFDerivAt_iff_isLittleO_nhds_zero, isQuotientMap, Bundle.Pretrivialization.continuousLinearMapCoordChange_apply, circleAverage_comp_comm, VectorPrebundle.contMDiffCoordChange_apply, isUniformEmbedding_of_bound, Submodule.orthogonalProjection_eq_linearProjOfIsCompl, HasCompactSupport.convolution_integrand_bound_right_of_subset, IsPositive.re_inner_nonneg_right, postcomp_compactConvergenceCLM_apply, integral_id_map, second_derivative_symmetric_of_eventually_of_real, BoundedContinuousFunction.toLp_denseRange, MeasureTheory.condExpL2_const_inner, HasRightInverse.surjective, TemperedDistribution.laplacianCLM_apply, toWOT_apply, curveIntegralFun_def, ext_ring_iff, norm_smulRightL_apply, ContinuousAlternatingMap.alternatizeUncurryFin_apply, intervalIntegral_comp_comm, contMDiffAt, zero_apply, isClosed_setOf_isCompactOperator, DoubleCentralizer.coe_snd, fpowerSeriesBilinear_apply_one, MeasureTheory.integral_convolution, le_opNorm_enorm, fderiv_norm_sq_apply, Submodule.starProjection_eq_self_iff, RCLike.imCLM_apply, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, ConvexOn.univ_sSup_of_nat_affine_eq, InnerProductGeometry.ConformalAt.preserves_angle, Submodule.starProjection_tendsto_closure_iSup, domain_mvt, MeasureTheory.Lp.toTemperedDistribution_smul_eq, NormedSpace.dual_def, SchwartzMap.laplacian_eq_fourierMultiplierCLM, HasFDerivAtFilter.hasDerivAtFilter, HasFDerivAt.isLittleOTVS, RCLike.geometric_hahn_banach_open_open, ContinuousAlternatingMap.ofSubsingleton_symm_apply_apply, fderiv_norm_sq, coe_mulₗᵢ, isUnit_iff_bijective, MDifferentiableOn.clm_bundle_apply₂, MeasureTheory.condExpL1_eq, OrthogonalFamily.projection_directSum_coeAddHom, innerSL_apply_comp, TopModuleCat.hom_forget₂_TopCat_map, conformalAt_iff', mdifferentiableAt, toSesqForm_apply_norm_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd, coeFn_holder, map_smul, coe_deriv₂, IsMIntegralCurveAt.eventually_hasDerivAt, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply, ContMDiffOn.clm_bundle_apply₂, MeasureTheory.Measure.ContinuousLinearMap.quasiMeasurePreserving, ContinuousWithinAt.clm_bundle_apply, extDeriv_apply, mfderiv_prod_eq_add_apply, MeasureTheory.condExpL2_indicator_nonneg, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply, geometric_hahn_banach_of_nonempty_interior, Bundle.ContinuousRiemannianMetric.isVonNBounded, comp_toSpanSingleton, HasStrictDerivAt.clm_apply, TemperedDistribution.smulLeftCLM_apply_apply, SeparatingDual.eq_iff_forall_dual_eq, HasFDerivWithinAt.isLittleO, closure_preimage, MeasureTheory.SimpleFunc.map_setToSimpleFunc, fderiv_inner_apply, hasDerivAt_of_bilinear, second_derivative_symmetric_of_eventually, HasFDerivAt.comp_hasDerivAt_of_eq, SeparationQuotient.outCLM_injective, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left', NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, HasLeftInverse.injective, continuousAt_uncurry_of_multilinear, BoundedContinuousFunction.probCharDual_apply, InnerProductSpace.norm_rankOne, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero, PiTensorProduct.mapLMultilinear_toFun_apply, VectorField.mlieBracket_smul_right, CStarMatrix.inner_toCLM_conjTranspose_right, iteratedDerivWithin_vcomp_three, antilipschitz_of_forall_le_inner_map, MDifferentiableAt.clm_apply, HasFDerivAt.isLittleO, fderiv_eq_smul_deriv, unitary.inner_map_map, CStarMatrix.toCLM_apply_single_apply, flipAlternating_apply_apply, coeFn_compLp', MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap, algebraMap_apply, comp_apply, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, coe_completion, iteratedFDeriv_succ_apply_left, ContDiffWithinAt.fderivWithin_apply, IsSymmSndFDerivAt.eq, norm_iteratedFDerivWithin_le_of_bilinear_aux, fderiv_inv', SeparationQuotient.outCLM_isUniformInducing, coeFn_ofIsClosedGraph, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, IsLocalMinOn.fderivWithin_eq_zero, RCLike.geometric_hahn_banach_open_point, Submodule.mem_iff_norm_starProjection, Complex.reCLM_apply, ContinuousLinearEquiv.ofBijective_apply_symm_apply, continuousMultilinearCurryFin1_apply, IsCoercive.antilipschitz, LinearMap.IsSymmetric.apply_clm, IsInvertible.inverse_apply_eq, norm_iteratedFDeriv_clm_apply_const
homeomorphOfUnit 📖	CompOp	2 math math: homeomorphOfUnit_apply, homeomorphOfUnit_symm_apply
id 📖	CompOp	119 math math: mfderiv_sumSwap, PiTensorProduct.mapL_id, snd_comp_inr, binomialSeries_eq_ordinaryHypergeometricSeries, Bundle.Trivial.symmL_trivialization, mfderivWithin_range_extChartAt_symm, ContinuousAlternatingMap.norm_ofSubsingleton_id_le, SeparationQuotient.mkCLM_comp_outCLM, fderivWithin_extChartAt_comp_extChartAt_symm_range, fderiv_id, hasFDerivAt_stereoInvFunAux, RCLike.map_same_eq_id, id_apply, ContinuousLinearEquiv.coe_comp_coe_symm, adjoint_id, LinearIsometry.id_toContinuousLinearMap, hasMFDerivAt_sumSwap, Bundle.Trivial.continuousLinearMapAt_trivialization, FormalMultilinearSeries.radius_compNeg, ModelWithCorners.hasMFDerivAt, hasMFDerivAt_inr, mfderivWithin_sumInr, fderivWithin_id, NormedSpace.inclusionInDoubleDual_norm_eq, hasMFDerivWithinAt_inr, pi_proj, isPositive_id, mfderivWithin_sumInl, exists_right_inverse_of_surjective, hasFDerivAt_id, iteratedFDerivWithin_smul_const_apply, PiTensorProduct.liftIsometry_tprodL, mfderiv_sumInl, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, fderiv_pow_ring, ContinuousLinearEquiv.coe_symm_comp_coe, TemperedDistribution.fourierMultiplierCLM_const, hasMFDerivAt_id, hasMFDerivWithinAt_id, ClosedSubmodule.comap_id, SchwartzMap.smulLeftCLM_const, hasFDerivWithinAt_pow', fderivWithin_id', SchwartzMap.compSubConstCLM_zero, SeparationQuotient.exists_out_continuousLinearMap, FormalMultilinearSeries.compContinuousLinearMap_id, mfderiv_extChartAt_self, OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, hasMFDerivAt_inl, TopModuleCat.hom_id, ProperCone.map_id, fderiv_pow_ring', ContinuousLinearEquiv.coe_refl, tangentBundleCore_coordChange_model_space, hasFDerivAt_pow, hasFDerivAt_single, ModelWithCorners.hasMFDerivWithinAt, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, ClosedSubmodule.map_id, fderiv_update, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id, SchwartzMap.fourierMultiplierCLM_const, ContinuousMultilinearMap.norm_ofSubsingleton_id_le, hasStrictFDerivAt_pow', ModelWithCorners.hasMFDerivWithinAt_symm, fst_comp_inl, Submodule.starProjection_orthogonal, hasFDerivAt_update, mfderiv_sumInr, iteratedFDeriv_smul_const_apply, fderiv_id', norm_id_le, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', hasFDerivAt_pow', mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', IsInvertible.inverse_comp_self, Submodule.starProjection_top, hasFDerivAt_sub_const, toContinuousAddMonoidHom_id, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, hasFDerivAtFilter_id, isConformalMap_id, intrinsicStar_id, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, ContinuousAlternatingMap.norm_ofSubsingleton_id, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, Submodule.id_eq_sum_starProjection_self_orthogonalComplement, FormalMultilinearSeries.ofScalars_comp_neg_id, fderivWithin_pow_ring', fst_prod_snd, coe_id', OrthonormalBasis.sum_rankOne_eq_id, norm_id, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id, id_comp, smulRight_id, nnnorm_id, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, ProperCone.comap_id, hasStrictFDerivAt_pow, IsInvertible.self_comp_inverse, coe_eq_id, hasFDerivWithinAt_pow, isConformalMap_const_smul, mfderivWithin_id, coe_id, mfderivWithin_sumSwap, fderivWithin_pow_ring, hasMFDerivWithinAt_inl, fderiv_single, inverse_id, one_def, comp_id, hasStrictFDerivAt_id, hasStrictFDerivAt_sub_const, coprod_inl_inr, ContinuousMultilinearMap.norm_ofSubsingleton_id, hasFDerivWithinAt_id, mfderiv_id
inhabited 📖	CompOp	1 math math: default_def
instMul 📖	CompOp	41 math math: Matrix.l2_opNorm_toEuclideanCLM, isStarProjection_iff_isSymmetricProjection, InnerProductSpace.isIdempotentElem_rankOne_self, Matrix.cstar_nnnorm_def, isStarNormal_iff_norm_eq_adjoint, LinearIsometryEquiv.conjStarAlgEquiv_apply, mul_apply, coe_mul', Submodule.isIdempotentElem_starProjection, Matrix.toEuclideanCLM_toLp, VonNeumannAlgebra.centralizer_centralizer', LinearIsometryEquiv.conjStarAlgEquiv_trans, isIdempotentElem_toLinearMap_iff, LinearIsometryEquiv.conjStarAlgEquiv_refl, IsIdempotentElem.TFAE, Matrix.inner_toEuclideanCLM, VonNeumannAlgebra.centralizer_centralizer, PiTensorProduct.mapL_mul, Matrix.ofLp_toEuclideanCLM, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, InnerProductSpace.isStarProjection_rankOne_self, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, isStarProjection_starProjection, LinearIsometryEquiv.symm_conjStarAlgEquiv, IsIdempotentElem.commute_iff_of_isUnit, DoubleCentralizer.mul_fst, IsIdempotentElem.commute_iff, isStarProjection_iff_isIdempotentElem_and_isStarNormal, LinearMap.isStarProjection_toContinuousLinearMap_iff, InnerProductSpace.isIdempotentElem_rankOne_self_iff, isStarProjection_iff_eq_starProjection_range, VonNeumannAlgebra.mem_commutant_iff, mul_def, VonNeumannAlgebra.coe_commutant, IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, coe_mul, isStarProjection_iff_eq_starProjection, Matrix.cstar_norm_def, DoubleCentralizer.mul_snd, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, LinearMap.IsSymmetricProjection.isStarProjection
instNatCast 📖	CompOp	4 math math: DoubleCentralizer.natCast_fst, isPositive_natCast, natCast_apply, DoubleCentralizer.natCast_snd
instSMul 📖	CompOp	346 math math: Matrix.l2_opNorm_toEuclideanCLM, HasStrictFDerivAt.log, HasStrictFDerivAt.fun_mul', HasMFDerivAt.mul, HasFDerivWithinAt.ccosh, Complex.restrictScalars_one_smulRight', HasFDerivWithinAt.ccos, Real.hasFDerivAt_fourierChar_neg_bilinear_left, hasStrictFDerivAt_exp_of_mem_ball, curveIntegral_smul, hasStrictFDerivAt_list_prod_finRange', HasStrictFDerivAt.csin, MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left, HasFDerivWithinAt.pow, fderivWithin_fun_smul, hasFDerivAt_multiset_prod, smul_apply, continuousSMul, Matrix.cstar_nnnorm_def, fderivWithin_csinh, HasDerivAtFilter.comp_hasFDerivAtFilter, HasDerivWithinAt.complexToReal_fderiv', ContMDiffCovariantDerivativeOn.affine_combination, fderivWithin_fun_pow', fderiv_multiset_prod, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, HasFDerivAt.fun_mul, TemperedDistribution.fourierMultiplierCLM_smul, HasDerivAt.comp_hasFDerivAt_of_eq, curveIntegralFun_smul, coe_smul', Differentiable.fderiv_norm_rpow, curveIntegrable_smul_iff, HasStrictFDerivAt.mul', fderiv_fun_pow, Complex.hasStrictFDerivAt_exp_real, fderiv_fun_smul, LinearIsometryEquiv.conjStarAlgEquiv_apply, HasStrictFDerivAt.pow, fderivWithin_sinh, HasStrictFDerivAt.const_mul, HasFDerivAt.finset_prod, smul_compLp, ContinuousAlternatingMap.curryLeft_smul, fderiv_const_smul_field, Real.hasStrictFDerivAt_rpow_of_pos, fderiv_fun_pow', HasFDerivWithinAt.csin, IsPositive.smul_of_nonneg, HasFDerivWithinAt.const_mul, HasFDerivWithinAt.fun_const_smul, HasStrictFDerivAt.const_smul, fderivWithin_ccosh, HasFDerivWithinAt.mul, fderivWithin_const_mul, HasFDerivWithinAt.multiset_prod, DoubleCentralizer.smul_toProd, HasFDerivAt.arctan, HasStrictFDerivAt.abs, HasFDerivAt.fun_smul, PiTensorProduct.mapL_smul, smul_comp, ContinuousAffineMap.smul_contLinear, HasDerivAt.comp_hasFDerivWithinAt, HasStrictFDerivAt.arsinh, HasFDerivWithinAt.exp, HasStrictFDerivAt.list_prod', fderivWithin_sin, Complex.hasStrictFDerivAt_cpow', SchwartzMap.smulLeftCLM_real_smul, HasMFDerivAt.smul, HasFDerivAt.fun_const_smul, curveIntegral_fun_smul, fderiv.log, hasStrictFDerivAt_multiset_prod, fderivWithin_finset_prod, fderiv_smul, flip_smul, HasFDerivWithinAt.const_smul, ContMDiffCovariantDerivativeOn.finite_affine_combination, NormedSpace.smul_mem_polar, IsCovariantDerivativeOn.smul_const, ContinuousAlternatingMap.alternatizeUncurryFin_smul, fderiv_mul_const', hasStrictFDerivAt_exp, HasFDerivWithinAt.fun_smul, hasFDerivAt_norm_rpow, Matrix.toEuclideanCLM_toLp, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, Complex.hasStrictFDerivAt_cpow, fderiv_pow, HasFDerivAt.pow, HasFDerivWithinAt.cpow, HasStrictFDerivAt.const_cpow, HasFDerivWithinAt.csinh, HasStrictFDerivAt.cexp, HasFDerivAt.abs, HasFDerivWithinAt.abs, uniformContinuousConstSMul, HasFDerivWithinAt.mul_const, fderiv_pow', fderiv_mul, DoubleCentralizer.smul_fst, fderivWithin_cos, toSpanSingleton_smul, fderivWithin_ccos, HasStrictFDerivAt.clog, fderiv_pow_ring, LinearIsometryEquiv.conjStarAlgEquiv_trans, HasStrictFDerivAt.sqrt, HasDerivWithinAt.complexToReal_fderiv, HasStrictFDerivAt.rpow, fderivWithin_fun_mul', TemperedDistribution.fourierMultiplierCLM_const, hasFDerivAt_list_prod', smulCommClass, fderiv_mul', fderivWithin_const_smul_of_field, HasStrictFDerivAt.ccos, HasFDerivWithinAt.cexp, LinearIsometryEquiv.conjStarAlgEquiv_refl, MeasureTheory.setToFun_smul_left, HasDerivAt.complexToReal_fderiv', HasDerivAt.complexToReal_fderiv, CovariantDerivative.affine_combination_toFun, fromTangentSpace_mfderiv_smul', IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, SchwartzMap.smulLeftCLM_const, Complex.hasFDerivAt_cpow, fderiv_const_smul_of_invertible, Matrix.inner_toEuclideanCLM, hasFDerivWithinAt_pow', HasFDerivAt.cexp, HasFDerivAt.ccos, HasFDerivWithinAt.log, HasFDerivAt.clog, fderivWithin_mul_const', fderivWithin_smul, hasFDerivAt_list_prod_finRange', IsCovariantDerivativeOn.leibniz, Complex.restrictScalars_one_smulRight, Matrix.ofLp_toEuclideanCLM, HasFDerivAt.ccosh, fderiv_cos, hasFDerivWithinAt_comp_smul_smul_iff, fderivWithin_fun_pow, HasStrictFDerivAt.arctan, HasFDerivAtFilter.const_smul, HasFDerivAt.multiset_prod, HasFDerivAt.mul_const, HasFDerivWithinAt.mul_const', HasDerivAt.comp_hasFDerivWithinAt_of_eq, fderiv_const_mul, fderiv_exp, fderiv_arctan, HasFDerivAtFilter.fun_const_smul, fderiv_pow_ring', fderivWithin.log, HasFDerivWithinAt.sinh, instStarModuleId, hasFDerivAt_pow, HasFDerivAt.log, isVonNBounded_iff, HasFDerivAt.exp, HasFDerivAt.fun_pow', HasMFDerivWithinAt.mul', IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d, fderiv_ccos, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, SchwartzMap.fourierMultiplierCLM_const, fderivWithin_const_smul_of_invertible, fderivWithin_exp, HasFDerivAt.const_mul, HasStrictDerivAt.complexToReal_fderiv', HasFDerivWithinAt.rpow_const, fderivWithin_multiset_prod, HasFDerivAt.mul, HasFDerivAt.sinh, hasStrictFDerivAt_pow', Complex.restrictScalars_toSpanSingleton, HasFDerivWithinAt.clog, hasFDerivAt_exp_smul_const_of_mem_ball, fderiv_fun_mul', HasFDerivAt.const_smul, HasFDerivAt.rpow_const, coord_norm', hasFDerivAt_exp_smul_const, HasStrictFDerivAt.const_rpow, continuousConstSMul, fderiv_finset_prod, hasStrictFDerivAt_list_prod_attach', restrictScalars_smul, HasStrictFDerivAt.cos, fromTangentSpace_mfderiv_smul, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, HasFDerivWithinAt.arsinh, InnerProductSpace.rankOne_comp_rankOne, HasStrictDerivAt.comp_hasStrictFDerivAt, HasDerivWithinAt.comp_hasFDerivWithinAt, comp_smulₛₗ, hasStrictFDerivAt_finset_prod, HasDerivWithinAt.comp_hasFDerivAt, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, HasFDerivAt.sin, HasFDerivAt.csin, HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq, fderiv_norm_smul, HasFDerivAt.hasFDerivAt_norm_smul, HasFDerivWithinAt.sqrt, HasFDerivWithinAt.pow', isScalarTower, fderivWithin_sqrt, HasFDerivAt.list_prod', fderivWithin_const_smul_field, fderiv_sinh, hasFDerivAt_pow', LinearIsometryEquiv.symm_conjStarAlgEquiv, HasFDerivWithinAt.const_cpow, HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq, HasFDerivWithinAt.arctan, HasFDerivWithinAt.rpow, HasMFDerivAt.prod, fderivWithin_csin, HasFDerivAt.cos, opNorm_smul_le, EuclideanGeometry.hasFDerivAt_inversion, HasStrictFDerivAt.fun_const_smul, fderivWithin_const_smul, HasFDerivAt.const_rpow, Matrix.toLin_finTwoProd_toContinuousLinearMap, fderiv_fun_const_smul, HasMFDerivWithinAt.mul, HasFDerivAt.arsinh, fderiv_ccosh, HasStrictFDerivAt.fun_smul, HasStrictFDerivAt.cpow, fderiv_fun_mul, HasFDerivAt.pow', HasStrictFDerivAt.pow', CurveIntegrable.smul, TopModuleCat.hom_smul, HasStrictFDerivAt.multiset_prod, HasFDerivWithinAt.smul, HasStrictFDerivAt.mul_const', IsConformalMap.smul, TestFunction.lineDerivCLM_smul, fderiv_sqrt, fderivWithin_list_prod', HasFDerivWithinAt.fun_mul', hasStrictFDerivAt_list_prod, fderivWithin_pow_ring', HasFDerivWithinAt.fun_pow', fderivWithin_mul_const, HasFDerivAt.mul_const', HasStrictFDerivAt.fun_pow', mfderiv_smul, HasStrictFDerivAt.sin, HasFDerivWithinAt.const_rpow, fderivWithin_cosh, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, Real.hasFDerivAt_fourierChar_neg_bilinear_right, ContinuousLinearEquiv.coord_norm', Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, hasStrictFDerivAt_exp_smul_const, Complex.hasStrictFDerivAt_log_real, HasStrictFDerivAt.mul, HasDerivAt.comp_hasFDerivAt, fderiv_mul_const, fderiv_csinh, smul_compLpL, HasFDerivAt.sqrt, HasFDerivAt.csinh, HasFDerivWithinAt.finset_prod, hasStrictFDerivAt_list_prod', HasStrictFDerivAt.ccosh, fderiv_norm_rpow, HasStrictFDerivAt.cosh, fderivWithin_pow, isCentralScalar, fderivWithin_fun_const_smul, hasStrictFDerivAt_pow, fderiv_comp_smul, fderivWithin_arctan, TemperedDistribution.smulLeftCLM_smul, MeasureTheory.charFun_map_eq_charFunDual_smul, Matrix.cstar_norm_def, fderiv_csin, fderiv_cosh, HasStrictFDerivAt.fun_mul, hasFDerivWithinAt_pow, HasFDerivWithinAt.mul', HasStrictFDerivAt.sinh, HasFDerivAt.cpow, Real.hasStrictFDerivAt_rpow_of_neg, IsCovariantDerivativeOn.affine_combination, MeasureTheory.weightedSMul_smul_measure, HasStrictDerivAt.complexToReal_fderiv, fderivWithin_mul', HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq, HasFDerivAt.cosh, isConformalMap_const_smul, VectorFourier.hasFDerivAt_fourierChar_smul, HasStrictFDerivAt.csinh, fderiv_const_smul_of_field, HasFDerivWithinAt.cos, coe_smul, fderiv_list_prod', HasMFDerivWithinAt.prod, fderivWithin_comp_smul, HasMFDerivAt.mul', hasFDerivAt_exp, fderivWithin_pow_ring, fderiv_const_smul, HasFDerivAt.fun_mul', HasStrictFDerivAt.mul_const, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, HasFDerivAt.mul', SchwartzMap.fourierMultiplierCLM_smul, hasFDerivAt_list_prod_attach', HasDerivWithinAt.comp_hasFDerivAt_of_eq, HasFDerivAt.rpow, fderivWithin_fun_mul, DoubleCentralizer.smul_snd, HasFDerivAt.smul, HasFDerivWithinAt.sin, SchwartzMap.smulLeftCLM_smul, HasStrictFDerivAt.exp, fderiv_sin, hasFDerivAt_exp_of_mem_ball, const_smul_mfderiv, HasMFDerivAt.const_smul, IsCovariantDerivativeOn.finite_affine_combination, MeasureTheory.L1.SimpleFunc.setToL1S_smul_left, fderivWithin_mul, HasFDerivWithinAt.fun_mul, HasStrictFDerivAt.smul, HasStrictFDerivAt.finset_prod, HasFDerivAt.const_cpow, HasFDerivWithinAt.cosh, comp_smul, HasStrictFDerivAt.rpow_const, hasStrictFDerivAt_exp_smul_const_of_mem_ball, Complex.restrictScalars_toSpanSingleton', HasFDerivWithinAt.list_prod', fderivWithin_pow', hasFDerivAt_finset_prod
monoidWithZero 📖	CompOp	38 math math: ContinuousLinearEquiv.unitsEquiv_apply, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, applySMulCommClass', smulRight_one_pow, DoubleCentralizer.pow_snd, Unitary.coe_linearIsometryEquiv_apply, Unitary.linearIsometryEquiv_coe_apply, unitary.linearIsometryEquiv_coe_symm_apply, ringInverse_equiv, Unitary.coe_symm_linearIsometryEquiv_apply, isUnit_of_forall_le_norm_inner_map, applyFaithfulSMul, homeomorphOfUnit_apply, toSpanSingleton_pow, coe_pow', HasFDerivAt.iterate, isUnit_iff_isUnit_toLinearMap, Unitary.linearIsometryEquiv_coe_symm_apply, HasStrictFDerivAt.iterate, coe_pow, HasFDerivWithinAt.iterate, DoubleCentralizer.pow_toProd, applySMulCommClass, Unitary.norm_map, DoubleCentralizer.pow_fst, unitary.norm_map, ringInverse_eq_inverse, homeomorphOfUnit_symm_apply, smul_def, Unitary.inner_map_map, inverse_eq_ringInverse, HasFDerivAtFilter.iterate, PiTensorProduct.mapL_pow, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, continuousConstSMul_apply, isUnit_iff_bijective, unitary.inner_map_map, unitary.linearIsometryEquiv_coe_apply
mulAction 📖	CompOp	1 math math: intrinsicStarModule
neg 📖	CompOp	77 math math: comp_neg, TemperedDistribution.lineDerivOpCLM_eq, binomialSeries_eq_ordinaryHypergeometricSeries, ContinuousAffineMap.neg_contLinear, curveIntegrable_fun_neg_iff, HasFDerivAtFilter.const_sub, curveIntegral_neg, fderivWithin_const_sub, HasFDerivAtFilter.neg, FormalMultilinearSeries.radius_compNeg, TemperedDistribution.smulLeftCLM_neg, fderivWithin_fun_neg, fderiv_neg, Real.fourier_iteratedFDeriv, HasMFDerivAt.neg, HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg, HasFDerivWithinAt.const_sub, coe_neg', hasFDerivAt_ringInverse, VectorFourier.fourierIntegral_iteratedFDeriv, HasMFDerivWithinAt.neg, hasMFDerivAt_neg, restrictScalars_neg, HasFDerivWithinAt.abs_of_neg, HasFDerivWithinAt.neg, DoubleCentralizer.neg_snd, fderiv_inverse, SchwartzMap.smulLeftCLM_fun_neg, fderivWithin_inv', HasStrictFDerivAt.abs_of_neg, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain, fderiv_norm_smul_neg, HasFDerivWithinAt.fun_neg, UpperHalfPlane.smulFDeriv_J_mul, HasStrictFDerivAt.neg, Real.fourier_fderiv, HasFDerivAt.abs_of_neg, curveIntegral_fun_neg, DoubleCentralizer.neg_toProd, curveIntegralFun_neg, HasStrictFDerivAt.const_sub, fderivWithin_neg, CurveIntegrable.fun_neg, curveIntegrable_neg_iff, ContDiffAt.hasStrictFDerivAt_implicitFunction, hasStrictFDerivAt_ringInverse, fderiv_fun_neg, Real.fourierIntegral_fderiv, fderiv_const_sub, HasFDerivAtFilter.fun_neg, SchwartzMap.smulLeftCLM_neg, toContinuousAddMonoidHom_neg, neg_apply, HasFDerivAt.fun_neg, HasStrictFDerivAt.fun_neg, neg_comp, coe_neg, HasFDerivAt.const_sub, FormalMultilinearSeries.ofScalars_comp_neg_id, HasFDerivAt.hasFDerivAt_norm_smul_neg, opNorm_neg, FormalMultilinearSeries.ofScalars_comp_neg, hasStrictFDerivAt_inv', VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, rayleighQuotient_neg_apply, hasFDerivAt_inv', exists_continuousLinearEquiv_fderiv_symm_eq, mfderiv_neg, HasFDerivAt.neg, TopModuleCat.hom_neg, exists_continuousLinearEquiv_fderivWithin_symm_eq, VectorFourier.fourierIntegral_fderiv, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fourierIntegral_iteratedFDeriv, CurveIntegrable.neg, DoubleCentralizer.neg_fst, fderiv_inv'
one 📖	CompOp	55 math math: Polynomial.fderiv, TangentBundle.continuousLinearMapAt_model_space, hasStrictFDerivAt_exp_of_mem_ball, smulRight_one_eq_toSpanSingleton, Submodule.starProjection_orthogonal', Complex.hasStrictFDerivAt_exp_real, hasStrictFDerivAt_exp_smul_const_of_mem_ball', PiTensorProduct.mapL_one, one_smulRight_eq_toSpanSingleton, Submodule.starProjection_top', hasStrictFDerivAt_exp, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, hasStrictFDerivAt_exp_smul_const', TangentBundle.coordChange_model_space, HasDerivWithinAt.complexToReal_fderiv, inner_map_map_iff_adjoint_comp_self, Polynomial.fderiv_aeval, HasDerivAt.complexToReal_fderiv, hasFDerivAt_exp_smul_const', Polynomial.hasFDerivAt, Complex.restrictScalars_one_smulRight, one_apply, IsMIntegralCurveAt.hasMFDerivAt, isometry_iff_adjoint_comp_self, DoubleCentralizer.one_snd, Polynomial.hasFDerivAt_aeval, hasFDerivAt_exp_zero, DoubleCentralizer.one_fst, Complex.restrictScalars_toSpanSingleton, hasFDerivAt_exp_smul_const_of_mem_ball, hasFDerivAt_exp_smul_const, hasStrictFDerivAt_exp_zero_of_radius_pos, TangentBundle.symmL_model_space, Polynomial.fderivWithin_aeval, Polynomial.fderivWithin, hasStrictFDerivAt_exp_zero, Polynomial.hasFDerivWithinAt_aeval, tendsto_birkhoffAverage_orthogonalProjection, normOneClass, DoubleCentralizer.one_toProd, hasFDerivAt_exp_smul_const_of_mem_ball', hasStrictFDerivAt_exp_smul_const, Complex.hasStrictFDerivAt_log_real, norm_map_iff_adjoint_comp_self, hasFDerivAt_exp_zero_of_radius_pos, UniformCauchySeqOnFilter.one_smulRight, Polynomial.hasFDerivWithinAt, HasStrictDerivAt.complexToReal_fderiv, isPositive_one, coe_one, hasFDerivAt_exp, one_def, hasFDerivAt_exp_of_mem_ball, hasStrictFDerivAt_exp_smul_const_of_mem_ball, LinearIsometry.adjoint_comp_self
projKerOfRightInverse 📖	CompOp	3 math math: coe_projKerOfRightInverse_apply, projKerOfRightInverse_comp_inv, projKerOfRightInverse_apply_idem
rangeRestrict 📖	CompOp	3 math math: coe_equivRange, coe_rangeRestrict, coe_linearMap_equivRange
restrictScalars 📖	CompOp	40 math math: Complex.restrictScalars_one_smulRight', isUniformEmbedding_restrictScalars, IsConformalMap.is_complex_or_conj_linear, coe_restrictScalars, coe_restrictScalarsₗ, bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, HasFDerivAt.restrictScalars, uniformContinuous_restrictScalars, restrictScalars_neg, continuous_restrictScalars, DifferentiableAt.fderiv_restrictScalars, coe_restrict_scalarsL', restrictScalars_add, curveIntegral_restrictScalars, Complex.restrictScalars_one_smulRight, HasStrictFDerivAt.restrictScalars, coe_restrictScalarsIsometry, HasFDerivWithinAt.restrictScalars, differentiableWithinAt_iff_restrictScalars, restrictScalars_sub, StrongDual.extendRCLikeₗᵢ_symm_apply, DifferentiableWithinAt.restrictScalars_fderivWithin, StrongDual.extendRCLikeₗ_symm_apply, Complex.restrictScalars_toSpanSingleton, restrictScalars_zero, restrictScalars_smul, isConformalMap_complex_linear_conj, isEmbedding_restrictScalars, toContinuousAddMonoidHom_restrictScalars, norm_restrictScalars, curveIntegralFun_restrictScalars, coe_restrictScalars', differentiableAt_iff_restrictScalars, isConformalMap_complex_linear, HasFDerivAtFilter.restrictScalars, bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp, isConformalMap_iff_is_complex_or_conj_linear, fderivWithin_restrictScalars_comp, curveIntegrable_restrictScalars_iff, Complex.restrictScalars_toSpanSingleton'
restrictScalarsₗ 📖	CompOp	3 math math: coe_restrictScalarsₗ, restrictScalarsIsometry_toLinearMap, coe_restrictScalarsL
semiring 📖	CompOp	40 math math: ContinuousLinearEquiv.conjContinuousAlgEquiv_refl, PiTensorProduct.mapLMonoidHom_apply, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, Unitization.splitMul_apply, DoubleCentralizer.nnnorm_def', applySMulCommClass', ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective, Unitization.nnnorm_def, DoubleCentralizer.norm_def', ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, instStarOrderedRing, ContinuousLinearEquiv.conjContinuousAlgEquiv_trans, toLinearMapRingHom_apply, Unitization.splitMul_injective_of_clm_mul_injective, applyFaithfulSMul, VonNeumannAlgebra.centralizer_centralizer', VonNeumannAlgebra.coe_mk, VonNeumannAlgebra.mem_carrier, Unitization.norm_eq_sup, DoubleCentralizer.algebraMap_snd, DoubleCentralizer.algebraMap_toProd, PositiveLinearMap.gnsStarAlgHom_apply, Algebra.IsCentral.instContinuousLinearMap, Unitization.norm_def, applySMulCommClass, instNonnegSpectrumClassRealId, DoubleCentralizer.algebraMap_fst, smul_def, Unitization.nnnorm_eq_sup, VonNeumannAlgebra.coe_toStarSubalgebra, Unitization.norm_splitMul_snd_sq, Unitization.splitMul_injective, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, continuousConstSMul_apply, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply, instStarOrderedRingRCLike, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply, DoubleCentralizer.toProdMulOppositeHom_apply, algebraMap_apply
smulRight 📖	CompOp	74 math math: Polynomial.fderiv, Complex.restrictScalars_one_smulRight', smulRight_one_eq_toSpanSingleton, fderivWithin_fun_smul, intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, HasDerivWithinAt.complexToReal_fderiv', intervalIntegral.fderiv_integral_of_tendsto_ae, hasStrictFDerivAt_exp_smul_const_of_mem_ball', fderiv_fun_smul, smulRight_zero, HasFDerivAt.fun_smul, one_smulRight_eq_toSpanSingleton, fderiv_smul, HasFDerivWithinAt.fun_smul, hasStrictFDerivAt_exp_smul_const', iteratedFDerivWithin_smul_const_apply, coe_smulRightₗ, InnerProductSpace.rankOne_def, Polynomial.fderiv_aeval, norm_smulRight_apply, toSpanSingleton_comp, SchwartzMap.smulRightCLM_apply_apply, HasDerivAt.complexToReal_fderiv', hasFDerivAt_exp_smul_const', intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, Polynomial.hasFDerivAt, intervalIntegral.integral_hasStrictFDerivAt, fderivWithin_smul, ContDiff.smulRight, IsCovariantDerivativeOn.leibniz, HasFDerivWithinAt.smul_const, IsMIntegralCurveAt.hasMFDerivAt, range_smulRight_apply, Polynomial.hasFDerivAt_aeval, HasFDerivAt.smul_const, HasStrictDerivAt.complexToReal_fderiv', hasFDerivAt_exp_smul_const_of_mem_ball, hasFDerivAt_exp_smul_const, fderiv_smul_const, iteratedFDeriv_smul_const_apply, intrinsicStar_smulRight, smulRight_comp_smulRight, Polynomial.fderivWithin_aeval, Polynomial.fderivWithin, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, intervalIntegral.fderivWithin_integral_of_tendsto_ae, intervalIntegral.integral_hasFDerivWithinAt, nnnorm_smulRight_apply, HasStrictFDerivAt.fun_smul, HasFDerivWithinAt.smul, ContDiffWithinAt.smulRight, Polynomial.hasFDerivWithinAt_aeval, fderivWithin_smul_const, det_smulRight, smulRight_id, smulRight_comp, hasFDerivAt_exp_smul_const_of_mem_ball', hasStrictFDerivAt_exp_smul_const, HasStrictFDerivAt.smul_const, ContDiffOn.smulRight, UniformCauchySeqOnFilter.one_smulRight, Polynomial.hasFDerivWithinAt, intervalIntegral.integral_hasFDerivAt, smulRight_apply, intervalIntegral.fderiv_integral, coe_smulRight, smulRightL_apply_apply, ContDiffAt.smulRight, isBoundedBilinearMap_smulRight, zero_smulRight, HasFDerivAt.smul, HasStrictFDerivAt.smul, hasStrictFDerivAt_exp_smul_const_of_mem_ball, Complex.restrictScalars_toSpanSingleton'
smulRightₗ 📖	CompOp	1 math math: coe_smulRightₗ
sub 📖	CompOp	49 math math: intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, IsCovariantDerivativeOn.difference_apply, intervalIntegral.fderiv_integral_of_tendsto_ae, Submodule.starProjection_orthogonal', HasFDerivAtFilter.sub, HasFDerivAt.sub, ApproximatesLinearOn.norm_fderiv_sub_le, fderiv_fun_sub, FDerivMeasurableAux.norm_sub_le_of_mem_A, IsCompactOperator.antilipschitz_of_not_hasEigenvalue, mfderiv_sub, HasFDerivWithinAt.fun_sub, fderivWithin_fun_sub, TemperedDistribution.smulLeftCLM_sub, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, ContinuousAffineMap.sub_contLinear, intervalIntegral.integral_hasStrictFDerivAt, sub_apply, HasFDerivAtFilter.fun_sub, sub_comp, fderiv_sub, restrictScalars_sub, le_def, HasStrictFDerivAt.fun_sub, DoubleCentralizer.sub_toProd, DoubleCentralizer.sub_fst, Submodule.starProjection_orthogonal, HasMFDerivAt.sub, HasFDerivWithinAt.sub, curveIntegralFun_sub, TopModuleCat.hom_sub, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, intervalIntegral.fderivWithin_integral_of_tendsto_ae, intervalIntegral.integral_hasFDerivWithinAt, toContinuousAddMonoidHom_sub, fderivWithin_sub, curveIntegral_fun_sub, coe_sub, coe_sub', DoubleCentralizer.sub_snd, SchwartzMap.smulLeftCLM_sub, comp_sub, ContinuousAffineMap.vsub_contLinear, curveIntegral_sub, intervalIntegral.integral_hasFDerivAt, CurveIntegrable.sub, intervalIntegral.fderiv_integral, HasStrictFDerivAt.sub, HasFDerivAt.fun_sub
toLinearMap 📖	CompOp	259 math math: TopModuleCat.hom_cokerπ, HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, coe_add, IsIdempotentElem.isClosed_range, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_fst, MeasureTheory.Measure.addHaar_image_continuousLinearMap, isSelfAdjoint_iff_isSymmetric, isStarProjection_iff_isSymmetricProjection, Complex.ofRealCLM_coe, ker_codRestrict, ImplicitFunctionData.isCompl_ker, equivProdOfSurjectiveOfIsCompl_toLinearEquiv, ContinuousLinearEquiv.snd_equivOfRightInverse, IsPositive.toLinearMap, LinearMap.adjoint_eq_toCLM_adjoint, ContinuousMap.range_toLp, coe_restrictScalars, ker_le_ker_iff_range_le_range, LinearMap.toContinuousLinearMap₁_coe, coe_snd, IsIdempotentElem.ext_iff, coe_inj, ProperCone.mem_map, SchauderBasis.range_proj_eq_span, isComplete_ker, coe_equivProdOfSurjectiveOfIsCompl, IsIdempotentElem.toLinearMap, LinearMap.mkContinuousOfExistsBound_coe, Submodule.IsOrtho.map_iff, HasStrictFDerivAt.eq_implicitFunctionOfComplemented, ImplicitFunctionData.range_leftDeriv, Submodule.range_starProjection, IsSelfAdjoint.isSymmetric, closedComplemented_ker_of_rightInverse, IsIdempotentElem.ker_mem_invtSubmodule, isClosed_genEigenspace, Complex.reCLM_coe, iInf_ker_proj, range_toLinearMap, coe_equivRange, Submodule.topologicalClosure_map, InnerProductSpace.isSymmetricProjection_rankOne_self, SeparatingDual.dualMap_surjective_iff, HasStrictFDerivAt.to_implicitFunctionOfComplemented, isClosed_ker, isPositive_def, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, ker_closedComplemented_of_finiteDimensional_range, LinearMap.toLinearMap_toContPerfPair, IsCoercive.range_eq_top, InnerProductSpace.trace_rankOne, DenseRange.topologicalClosure_map_submodule, toLinearMapRingHom_apply, MeasureTheory.Measure.addHaar_preimage_continuousLinearMap, NormedSpace.toLinearMap_inclusionInDoubleDualWeak, Matrix.linfty_opNNNorm_toMatrix, Module.Basis.coe_constrL, Submodule.range_subtypeL, SchauderBasis.finrank_range_proj, coe_coprod, PiTensorProduct.mapL_coe, IsSelfAdjoint.hasEigenvector_of_isMaxOn, LinearMap.IsSymmetric.coe_toSelfAdjoint, LinearEquiv.coe_toContinuousLinearEquiv_symm, coe_codRestrict, isPositive_toLinearMap_iff, RCLike.reCLM_coe, HasStrictFDerivAt.map_implicitFunction_eq, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply_ker, coe_ofSeqClosedGraph, IsPositive.isSymmetric, closed_complemented_range_of_isCompl_of_ker_eq_bot, equivRange_symm_apply, InnerProductSpace.rank_rankOne, IsCompactOperator.hasEigenvalue_or_mem_resolventSet, Submodule.toLinearMap_starProjection_eq_isComplProjection, coe_coe, coe_projKerOfRightInverse_apply, IsStarNormal.ker_adjoint_eq_ker, ClosedSubmodule.orthogonal_eq_inter, toLinearMap_intrinsicStar, isIdempotentElem_toLinearMap_iff, Submodule.coe_continuous_linearProjOfClosedCompl, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, coe_inr, PiTensorProduct.liftEquiv_symm_apply, IsStarNormal.orthogonal_range, IsIdempotentElem.TFAE, coe_rangeRestrict, LinearMap.range_toContinuousLinearMap, equivRange_symm_toLinearEquiv, Submodule.starProjection_isSymmetric, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, coe_comp, LinearMap.coe_toContinuousLinearMap, isUnit_iff_isUnit_toLinearMap, toLinearMap_innerSL_apply, coe_pi, continuous_toLinearMap, LinearMap.toContinuousLinearMap_eq_iff_eq_toLinearMap, coe_linearMap_equivRange, LinearIsometryEquiv.completeSpace_map, coeLM_apply, toPMap_adjoint_eq_adjoint_toPMap_of_dense, ContinuousAffineMap.coe_contLinear_eq_linear, WithLp.coe_fstL, HasStrictFDerivAt.to_implicitFunction, range_smulRight_apply, toLinearMap_eq_iff_eq_toContinuousLinearMap, PointwiseConvergenceCLM.coeLMₛₗ_apply, compLeftContinuous_apply, toLinearMap_algebraMapCLM, toLinearMap_toSpanSingleton, coe_pow, PointwiseConvergenceCLM.coeLM_apply, ker_self_comp_adjoint, ContinuousLinearEquiv.ofSubmodule'_apply, VonNeumannAlgebra.IsIdempotentElem.mem_iff, Complex.conjCLE_coe_toLinearMap, SchauderBasis.RankOneDecomposition.finrank_range, ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, orthogonalComplement_iSup_eigenspaces_eq_bot, SchauderBasis.finrank_range_succSub_eq_one, IsStarProjection.ext_iff, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, Submodule.isSymmetricProjection_starProjection, LinearMap.mkContinuous_coe, isSelfAdjoint_toLinearMap_iff, VonNeumannAlgebra.IsStarProjection.mem_iff, MeasureTheory.Measure.addHaar_image_continuousLinearEquiv, Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, ker_prod, Submodule.topologicalClosure_mem_invtSubmodule, sub_apply', PiTensorProduct.mapL_apply, LinearIsometryEquiv.submoduleMap_symm_apply_coe, Submodule.ker_subtypeL, Submodule.IsOrtho.comap_iff, InnerProductSpace.toMatrix_rankOne, ClosedSubmodule.toSubmodule_comap, InnerProductSpace.isSymmetric_rankOne_self, LinearEquiv.coe_toContinuousLinearEquiv, ProperCone.coe_map, ImplicitFunctionData.range_rightDeriv, range_mfderiv_coe_sphere, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self, ker_adjoint_comp_self, isClosed_eigenspace, projKerOfRightInverse_comp_inv, Submodule.ker_starProjection, ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap, Matrix.linfty_opNorm_toMatrix, IsIdempotentElem.commute_iff_of_isUnit, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_fst, coe_restrictScalarsL, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_apply_ker, Submodule.ker_orthogonalProjection, IsIdempotentElem.range_mem_invtSubmodule_iff, MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv, HasLeftInverse.closedComplemented_range, ContinuousLinearEquiv.submoduleMap_symm_apply, Complex.imCLM_coe, orthogonal_range, WithLp.coe_sndL, IsIdempotentElem.commute_iff, range_eq_map_coprodSubtypeLEquivOfIsCompl, spectrum_eq, isPositive_iff, IsSelfAdjoint.hasEigenvector_of_isMinOn, coeLMₛₗ_apply, IsIdempotentElem.range_mem_invtSubmodule, projKerOfRightInverse_apply_idem, toAddMonoidHom_completion, coe_proj, coe_neg, InnerProductSpace.toLinearMap_rankOne, cont, closed_range_of_antilipschitz, coe_sub, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, TopModuleCat.kerι_apply, ContinuousLinearEquiv.submoduleMap_apply, IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, IsCoercive.ker_eq_bot, ker_prod_ker_le_ker_coprod, RCLike.imCLM_coe, isStarProjection_iff_eq_starProjection_range, EuclideanGeometry.orthogonalProjection_linear, ContinuousLinearEquiv.ofSubmodule'_symm_apply, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, completeSpace_ker, HasLeftInverse.isCompl_complement, coe_sum, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, coe_fst, GeneralSchauderBasis.range_proj_eq_span, coe_inl, coe_le_coe_iff, IsStarProjection.isSymmetricProjection, range_prod_eq, coe_prodMap, AntilipschitzWith.completeSpace_range_clm, LinearMap.coe_toContinuousLinearMap_symm, coe_mul, Submodule.orthogonal_eq_inter, coe_injective, LinearMap.clmOfExistsBoundedImage_coe, coe_eq_id, ker_coprod_of_disjoint_range, finite_dimensional_eigenspace, HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image, RCLike.ofRealCLM_coe, ProbabilityTheory.isPositive_covarianceOperator, coe_smulRight, coe_mk, Submodule.starProjection_coe_eq_isCompl_projection, algebraMapCLM_toLinearMap, IsIdempotentElem.hasOrthogonalProjection_range, coe_smul, apply_val_ker, orthogonal_mem_invtSubmodule, HasStrictFDerivAt.implicitFunction_apply_image, bijective_iff_dense_range_and_antilipschitz, coe_one, range_coprod, coe_id, BoundedContinuousFunction.range_toLp, ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap, ContinuousLinearEquiv.fst_equivOfRightInverse, coe_ofIsClosedGraph, Submodule.coe_subtypeL, Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl, coe_prod, LinearMap.canLiftContinuousLinearMap, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, coe_piMap, SchauderBasis.RankOneDecomposition.e_mem_range, InnerProductSpace.symm_toEuclideanLin_rankOne, IsIdempotentElem.ker_mem_invtSubmodule_iff, mem_invtSubmodule_adjoint_iff, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, IntrinsicStar.isSelfAdjoint_toLinearMap_iff, IsCoercive.isClosed_range, isOpen_setOf_nat_le_rank, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source, HasStrictFDerivAt.eq_implicitFunction, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, GeneralSchauderBasis.finrank_range_proj, orthogonal_ker, LinearMap.ker_toContinuousLinearMap, coe_zero, mkOfIsCompactOperator_to_linearMap, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, LinearIsometryEquiv.submoduleMap_apply_coe
toLinearMapRingHom 📖	CompOp	1 math math: toLinearMapRingHom_apply
toSpanSingleton 📖	CompOp	58 math math: toSpanSingleton_zero, Complex.restrictScalars_one_smulRight', smulRight_one_eq_toSpanSingleton, derivWithin_fderivWithin, intrinsicStar_toSpanSingleton, smulRight_one_pow, hasFDerivWithinAt_inv, toSpanSingleton_apply, toSpanSingleton_apply_one, HasDerivWithinAt.hasFDerivWithinAt, HasMFDerivAt.smul, one_smulRight_eq_toSpanSingleton, deriv_fderiv, norm_toSpanSingleton, nnnorm_toSpanSingleton, HasDerivAt.hasFDerivAt, toSpanSingleton_apply_map_one, hasDerivWithinAt_iff_hasFDerivWithinAt, toSpanSingleton_pow, toSpanSingleton_smul, det_toSpanSingleton, toSpanSingleton_comp, fromTangentSpace_mfderiv_smul', toSpanSingletonLE_apply, Complex.restrictScalars_one_smulRight, HasStrictDerivAt.hasStrictFDerivAt, toLinearMap_toSpanSingleton, hasStrictFDerivAt_inv, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, fderiv_inv, hasDerivAt_iff_hasFDerivAt, InnerProductSpace.rankOne_def', toSpanSingleton_one, Complex.restrictScalars_toSpanSingleton, fromTangentSpace_mfderiv_smul, toSpanSingleton_comp_toSpanSingleton, adjoint_toSpanSingleton, toSpanSingleton_derivWithin, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, toSpanSingleton_add, fderivWithin_inv, det_one_smulRight, hasDerivAtFilter_iff_hasFDerivAtFilter, toSpanSingleton_deriv, HasDerivAtFilter.hasFDerivAtFilter, toSpanSingleton_one_eq_algebraMapCLM, smulRight_one_eq_iff, smulRight_id, mfderiv_smul, smulRight_one_one, lsmul_flip_apply, hasStrictDerivAt_iff_hasStrictFDerivAt, toSpanSingleton_inj, MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp, hasFDerivAt_inv, adjoint_innerSL_apply, comp_toSpanSingleton, Complex.restrictScalars_toSpanSingleton'
toSpanSingletonLE 📖	CompOp	2 math math: toSpanSingletonLE_apply, toSpanSingletonLE_symm_apply
uniqueOfLeft 📖	CompOp	—
uniqueOfRight 📖	CompOp	—
zero 📖	CompOp	183 math math: toSpanSingleton_zero, TopModuleCat.hom_zero, fderivWithin_ofNat, Submodule.IsOrtho.starProjection_comp_starProjection, fderiv_intCast, fderivWithin_one, hasFDerivWithinAt_const, hasFDerivAt_one, SchauderBasis.proj_zero, ContinuousAffineMap.const_contLinear, fderivWithin_zero_of_not_accPt, DoubleCentralizer.zero_snd, nhds_zero_eq_of_basis, TestFunction.monoCLM_eq_zero, CurveIntegrable.zero, Submodule.starProjection_comp_starProjection_eq_zero_iff, coe_zero', IsLocalMax.fderiv_eq_zero, hasBasis_nhds_zero, fderivWithin_intCast, HasFDerivAt.of_notMem_tsupport, fderiv_ofNat, fderivWithin_zero, hasStrictFDerivAt_natCast, hasFDerivAtFilter_ofNat, hasFDerivAtFilter_zero, Submodule.IsOrtho.orthogonalProjection_comp_subtypeL, smulRight_zero, Submodule.orthogonalProjection_bot, MeasureTheory.L1.setToL1_zero_left, HasCompactSupport.fderiv, hasFDerivWithinAt_intCast, ProbabilityTheory.covarianceOperator_zero, curveIntegral_fun_zero, hasFDerivAtFilter_const, HasFDerivWithinAt.of_notMem_tsupport, IsLocalExtr.fderiv_eq_zero, hasFDerivAt_of_subsingleton, HasStrictFDerivAt.of_notMem_tsupport, isInvertible_zero_iff, pi_eq_zero, ProbabilityTheory.covarianceBilin_zero, InnerProductSpace.rankOne_eq_zero, fderiv_one, toContinuousAddMonoidHom_zero, ProbabilityTheory.covarianceBilinDual_zero, NormedSpace.polar_ball_subset_closedBall_div, compContinuousLinearMap_zero, MeasureTheory.weightedSMul_empty, rayleighQuotient_zero_apply, bilinearComp_zero_right, nonneg_iff_isPositive, MeasureTheory.weightedSMul_null, CurveIntegrable.fun_zero, fderiv_mem_iff, zero_comp, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, MeasureTheory.setToFun_zero_left, IsLocalMax.hasFDerivAt_eq_zero, eventually_nhds_zero_mapsTo, extDerivFun_zero, hasFDerivWithinAt_one, InnerProductSpace.continuousLinearMapOfBilin_zero, hasFDerivAt_ofNat, BoundedContinuousFunction.probCharDual_zero, hasFDerivWithinAt_zero, hasFDerivWithinAt_singleton, ContinuousAffineMap.contLinear_eq_zero_iff_exists_const, fderivWithin_zero_of_notMem_closure, hasStrictFDerivAt_zero, Submodule.starProjection_bot, fderivWithin_const, CovariantDerivative.zero, fderiv_natCast, intrinsicStar_zero, fderiv_const, hasMFDerivAt_const, GeneralSchauderBasis.proj_empty, hasFDerivAt_single, isVonNBounded_iff, mfderivWithin_zero_of_not_mdifferentiableWithinAt, curveIntegralFun_fun_zero, bilinearComp_zero, inverse_zero, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d, DoubleCentralizer.zero_fst, default_def, fderiv_update, hasFDerivAt_zero_of_eventually_const, hasFDerivAt_const, Asymptotics.IsBigO.hasFDerivWithinAt, CovariantDerivative.torsion_eq_zero_iff, mfderivWithin_const, StrongDual.polar_univ, ContinuousAlternatingMap.curryLeft_zero, fderivWithin_fun_const, hasMFDerivWithinAt_const, restrictScalars_zero, hasFDerivAt_update, fst_comp_inr, fderiv_zero_of_not_differentiableAt, opNorm_zero, curveIntegral_zero, hasBasis_nhds_zero_of_basis, tsupport_fderiv_subset, SchauderBasis.RankOneDecomposition.proj_zero, SchwartzMap.tsupport_fderivCLM_subset, opNorm_zero_iff, mfderiv_zero_of_not_mdifferentiableAt, MeasureTheory.SimpleFunc.setToSimpleFunc_zero, hasFDerivWithinAt_natCast, fderivWithin_natCast, NormedSpace.polar_ball, MeasureTheory.L1.SimpleFunc.setToL1S_zero_left, ProbabilityTheory.covarianceBilin_of_not_memLp, ContDiffMapSupportedIn.monoCLM_eq_zero, comp_zero, hasStrictFDerivAt_one, NormedSpace.sInter_polar_eq_closedBall, hasFDerivAt_natCast, hasFDerivAt_intCast, TestFunction.fderivCLM_apply_of_gt, fderiv_zero, nhds_zero_eq, DoubleCentralizer.zero_toProd, inverse_of_not_isInvertible, bilinearComp_zero_left, hasFDerivWithinAt_ofNat, ContDiffMapSupportedIn.fderivLM_apply, extend_zero, IsCovariantDerivativeOn.zero, StrongDual.zero_mem_polar, hasStrictFDerivAt_ofNat, ProbabilityTheory.uncenteredCovarianceBilin_zero, mfderiv_const, hasStrictFDerivAt_list_prod, ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, IsLocalMin.hasFDerivAt_eq_zero, snd_comp_inl, fderivWithin_const_apply, norm_sub_le_mul_volume_of_norm_fderiv_le, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left, eq_zero_of_forall_hasEigenvalue_eq_zero, NormedSpace.closedBall_inv_subset_polar_closedBall, Bundle.Pretrivialization.continuousLinearMap_symm_apply', hasFDerivAt_zero, flip_zero, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, isPositive_zero, hasFDerivAtFilter_natCast, jacobiTheta₂_fderiv_undef, fderiv_of_notMem_tsupport, hasStrictFDerivAt_const, IsLocalMin.fderiv_eq_zero, fderivWithin_zero_of_not_differentiableWithinAt, NormedSpace.polar_closedBall, fderivWithin_def, support_fderiv_subset, TestFunction.lineDerivCLM_apply_of_gt, fderiv_fun_const, pi_zero, Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff, hasFDerivWithinAt_of_subsingleton, MeasureTheory.condExpInd_empty, hasStrictFDerivAt_intCast, ContinuousAffineMap.zero_contLinear, MeasureTheory.weightedSMul_zero_measure, IsLocalExtr.hasFDerivAt_eq_zero, fderiv_single, fderivWithin_mem_iff, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, Bundle.Pretrivialization.continuousLinearMapCoordChange_apply, zero_smulRight, zero_apply, ProbabilityTheory.covarianceOperator_of_not_memLp, fderiv_const_apply, Asymptotics.IsBigO.hasFDerivAt, HasMFDerivWithinAt.mfderivWithin_eq_zero, coe_zero, curveIntegralFun_zero, hasFDerivAtFilter_intCast, hasFDerivAtFilter_one
«term_∘L_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
add_comp 📖	mathematical	—	comp ContinuousLinearMap add	—	ext
algebraMap_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike RingHom CommSemiring.toSemiring semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup RingHom.instFunLike algebraMap algebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsTopologicalAddGroup.toContinuousAdd
applyFaithfulSMul 📖	mathematical	—	FaithfulSMul ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid monoidWithZero Module.toDistribMulAction semiring applyModule	—	ext
applySMulCommClass 📖	mathematical	—	SMulCommClass ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction monoidWithZero semiring applyModule	—	map_smul
applySMulCommClass' 📖	mathematical	—	SMulCommClass ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid monoidWithZero Module.toDistribMulAction semiring applyModule Semiring.toMonoidWithZero	—	map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
apply_val_ker 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike Submodule SetLike.instMembership Submodule.setLike LinearMap.ker toLinearMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
cancel_left 📖	—	DFunLike.coe ContinuousLinearMap funLike comp	—	—	ext
closedComplemented_ker_of_rightInverse 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike	Submodule.ClosedComplemented LinearMap.ker Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring toLinearMap	—	RingHomInvPair.ids projKerOfRightInverse_apply_idem
coeFn_injective 📖	mathematical	—	ContinuousLinearMap DFunLike.coe funLike	—	DFunLike.coe_injective
coeLM_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap addCommMonoid LinearMap.addCommMonoid module LinearMap.module LinearMap.instFunLike coeLM toLinearMap	—	—
coeLMₛₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap addCommMonoid LinearMap.addCommMonoid module LinearMap.module LinearMap.instFunLike coeLMₛₗ toLinearMap	—	—
coe_add 📖	mathematical	—	toLinearMap ContinuousLinearMap add LinearMap LinearMap.instAdd	—	—
coe_add' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike add Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_codRestrict 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearMap funLike	toLinearMap Submodule SetLike.instMembership Submodule.setLike instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module codRestrict LinearMap.codRestrict	—	—
coe_codRestrict_apply 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearMap funLike	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module funLike codRestrict	—	—
coe_coe 📖	mathematical	—	DFunLike.coe LinearMap LinearMap.instFunLike toLinearMap ContinuousLinearMap funLike	—	—
coe_comp 📖	mathematical	—	toLinearMap comp LinearMap.comp	—	—
coe_comp' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe ContinuousLinearMap funLike	DFunLike.coe ContinuousLinearMap funLike copy	—	—
coe_eq_id 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.id id	—	coe_id
coe_id 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring id LinearMap.id	—	—
coe_id' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike id	—	—
coe_inj 📖	mathematical	—	toLinearMap	—	coe_injective
coe_injective 📖	mathematical	—	ContinuousLinearMap LinearMap toLinearMap	—	—
coe_mk 📖	mathematical	Continuous AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom	toLinearMap	—	—
coe_mk' 📖	mathematical	Continuous AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom	DFunLike.coe ContinuousLinearMap funLike LinearMap LinearMap.instFunLike	—	—
coe_mul 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap instMul LinearMap Module.End.instMul	—	—
coe_mul' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike instMul	—	—
coe_neg 📖	mathematical	—	toLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap neg LinearMap LinearMap.instNeg	—	—
coe_neg' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike neg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_one 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap one LinearMap Module.End.instOne	—	—
coe_pow 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap Monoid.toPow MonoidWithZero.toMonoid monoidWithZero LinearMap Module.End.instMonoid	—	DFunLike.ext' coe_pow' hom_coe_pow
coe_pow' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike Monoid.toPow MonoidWithZero.toMonoid monoidWithZero Nat.iterate	—	hom_coe_pow
coe_projKerOfRightInverse_apply 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.ker toLinearMap DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module funLike projKerOfRightInverse SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_rangeRestrict 📖	mathematical	—	toLinearMap Submodule SetLike.instMembership Submodule.setLike LinearMap.range instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module rangeRestrict LinearMap.rangeRestrict	—	—
coe_restrictScalars 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring restrictScalars LinearMap.restrictScalars	—	—
coe_restrictScalars' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike restrictScalars	—	—
coe_restrictScalarsₗ 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap addCommMonoid module LinearMap.instFunLike restrictScalarsₗ restrictScalars	—	—
coe_smul 📖	mathematical	—	toLinearMap ContinuousLinearMap instSMul LinearMap LinearMap.instSMul	—	—
coe_smul' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass	—	—
coe_smulRight 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring smulRight LinearMap.smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
coe_smulRightₗ 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap addCommMonoid module LinearMap.instFunLike smulRightₗ smulRight	—	—
coe_sub 📖	mathematical	—	toLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap sub LinearMap LinearMap.instSub	—	—
coe_sub' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike sub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_sum 📖	mathematical	—	toLinearMap Finset.sum ContinuousLinearMap addCommMonoid LinearMap LinearMap.addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
coe_sum' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike Finset.sum addCommMonoid Pi.addCommMonoid	—	coe_sum LinearMap.coe_sum Finset.sum_congr
coe_zero 📖	mathematical	—	toLinearMap ContinuousLinearMap zero LinearMap LinearMap.instZero	—	—
coe_zero' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike zero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
comp_add 📖	mathematical	—	comp ContinuousLinearMap add	—	ext map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
comp_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_finset_sum 📖	mathematical	—	comp Finset.sum ContinuousLinearMap addCommMonoid	—	ext coe_sum' Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass Finset.sum_congr
comp_id 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids id	—	ext RingHomCompTriple.ids
comp_neg 📖	mathematical	—	comp Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap neg	—	ext map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
comp_smul 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearMap instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	ext RingHomCompTriple.ids map_smul_of_tower
comp_smulₛₗ 📖	mathematical	—	comp ContinuousLinearMap instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	ext MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
comp_sub 📖	mathematical	—	comp Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap sub	—	ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
comp_toSpanSingleton 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHomCompTriple.ids toSpanSingleton DFunLike.coe ContinuousLinearMap funLike	—	RingHomCompTriple.ids LinearMap.comp_toSpanSingleton
comp_zero 📖	mathematical	—	comp ContinuousLinearMap zero	—	ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
completeSpace_eqLocus 📖	mathematical	—	CompleteSpace Submodule SetLike.instMembership Submodule.setLike LinearMap.eqLocus ContinuousLinearMap UniformSpace.toTopologicalSpace funLike ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass instUniformSpaceSubtype	—	IsClosed.completeSpace_coe ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass isClosed_eq ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass
completeSpace_ker 📖	mathematical	—	CompleteSpace Submodule SetLike.instMembership Submodule.setLike LinearMap.ker toLinearMap UniformSpace.toTopologicalSpace instUniformSpaceSubtype	—	IsComplete.completeSpace_coe isComplete_ker
cont 📖	mathematical	—	Continuous AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom toLinearMap	—	—
continuous 📖	mathematical	—	Continuous DFunLike.coe ContinuousLinearMap funLike	—	cont
continuousConstSMul_apply 📖	mathematical	—	ContinuousConstSMul ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid monoidWithZero Module.toDistribMulAction semiring applyModule	—	continuous
continuousSemilinearMapClass 📖	mathematical	—	ContinuousSemilinearMapClass ContinuousLinearMap funLike	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass LinearMap.map_smul' cont
continuous_toLinearMap 📖	mathematical	—	Continuous DFunLike.coe LinearMap LinearMap.instFunLike toLinearMap	—	cont
copy_eq 📖	mathematical	DFunLike.coe ContinuousLinearMap funLike	copy	—	DFunLike.ext'
default_def 📖	mathematical	—	ContinuousLinearMap inhabited zero	—	—
eqOn_closure_span 📖	mathematical	Set.EqOn DFunLike.coe ContinuousLinearMap funLike	Set.EqOn DFunLike.coe ContinuousLinearMap funLike closure SetLike.coe Submodule Submodule.setLike Submodule.span	—	Set.EqOn.closure LinearMap.eqOn_span' continuous
exists_ne_zero 📖	—	—	—	—	ext
ext 📖	—	DFunLike.coe ContinuousLinearMap funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike	—	ext
ext_on 📖	—	Dense SetLike.coe Submodule Submodule.setLike Submodule.span Set.EqOn DFunLike.coe ContinuousLinearMap funLike	—	—	ext eqOn_closure_span
ext_ring 📖	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	LinearMap.ext_ring
ext_ring_iff 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext_ring
finset_sum_comp 📖	mathematical	—	comp Finset.sum ContinuousLinearMap addCommMonoid	—	ext coe_sum' Finset.sum_apply Finset.sum_congr
homeomorphOfUnit_apply 📖	mathematical	—	DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike homeomorphOfUnit ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike Units.val MonoidWithZero.toMonoid monoidWithZero	—	—
homeomorphOfUnit_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeomorphOfUnit ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike Units.val MonoidWithZero.toMonoid monoidWithZero Units Units.instInv	—	—
id_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike id	—	—
id_comp 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids id	—	ext RingHomCompTriple.right_ids
instNontrivialId 📖	mathematical	—	Nontrivial ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring	—	exists_ne DFunLike.congr_fun
intCast_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike AddGroupWithOne.toIntCast Ring.toAddGroupWithOne ring SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
isCentralScalar 📖	mathematical	—	IsCentralScalar ContinuousLinearMap instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring SMulCommClass.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass ContinuousConstSMul.op	—	SMulCommClass.op_right ContinuousConstSMul.op ext IsCentralScalar.op_smul_eq_smul
isClosed_ker 📖	mathematical	—	IsClosed SetLike.coe Submodule Submodule.setLike LinearMap.ker toLinearMap	—	continuous_iff_isClosed ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass continuousSemilinearMapClass isClosed_singleton
isComplete_ker 📖	mathematical	—	IsComplete SetLike.coe Submodule Submodule.setLike LinearMap.ker toLinearMap UniformSpace.toTopologicalSpace	—	IsClosed.isComplete isClosed_ker
isHomeomorph_of_isUnit 📖	mathematical	IsUnit ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring MonoidWithZero.toMonoid monoidWithZero	IsHomeomorph DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	Homeomorph.isHomeomorph
isIdempotentElem_toLinearMap_iff 📖	mathematical	—	IsIdempotentElem LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMul toLinearMap ContinuousLinearMap instMul	—	RingHomCompTriple.ids
isOpenMap_of_ne_zero 📖	mathematical	—	IsOpenMap DFunLike.coe StrongDual DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	exists_ne_zero IsOpenMap.of_sections Continuous.continuousAt Continuous.const_add instSeparatelyContinuousAddOfContinuousAdd Continuous.smul Continuous.sub continuous_id' continuous_const sub_self zero_smul add_zero map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass inv_mul_cancel₀ mul_one add_sub_cancel
isScalarTower 📖	mathematical	—	IsScalarTower ContinuousLinearMap instSMul	—	ext smul_assoc
ker_codRestrict 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearMap funLike	LinearMap.ker Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module toLinearMap instTopologicalSpaceSubtype codRestrict	—	LinearMap.ker_codRestrict
leftInverse_of_comp 📖	mathematical	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids id	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	RingHomCompTriple.ids
map_add 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
map_neg 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
map_smul 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
map_smul_of_tower 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	LinearMap.CompatibleSMul.map_smul
map_smulₛₗ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	LinearMap.map_smulₛₗ
map_sub 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
map_zero 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
mul_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike instMul	—	—
mul_def 📖	mathematical	—	ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instMul comp RingHomCompTriple.ids	—	—
natCast_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike instNatCast AddMonoid.toNSMul AddCommMonoid.toAddMonoid	—	—
neg_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
neg_comp 📖	mathematical	—	comp Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap neg	—	ext
ofNat_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike AddMonoid.toNSMul AddCommMonoid.toAddMonoid	—	—
one_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike one	—	—
one_def 📖	mathematical	—	ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring one id	—	—
one_smulRight_eq_toSpanSingleton 📖	mathematical	—	smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction ContinuousLinearMap RingHom.id one toSpanSingleton	—	smulRight_one_eq_toSpanSingleton
projKerOfRightInverse_apply_idem 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Submodule SetLike.instMembership Submodule.setLike LinearMap.ker toLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module funLike projKerOfRightInverse	—	apply_val_ker map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass sub_zero
projKerOfRightInverse_comp_inv 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Submodule SetLike.instMembership Submodule.setLike LinearMap.ker toLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module funLike projKerOfRightInverse Submodule.zero	—	sub_self
range_coeFn_eq 📖	mathematical	—	Set.range ContinuousLinearMap DFunLike.coe funLike Set Set.instInter setOf Continuous LinearMap LinearMap.instFunLike	—	Set.ext continuous
range_smulRight_apply 📖	mathematical	—	LinearMap.range DivisionSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap smulRight Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.span Set Set.instSingletonSet	—	LinearMap.range_smulRight_apply
range_toLinearMap 📖	mathematical	—	Set.range DFunLike.coe LinearMap LinearMap.instFunLike toLinearMap ContinuousLinearMap funLike	—	—
restrictScalars_add 📖	mathematical	—	restrictScalars ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring add	—	—
restrictScalars_neg 📖	mathematical	—	restrictScalars Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring neg	—	—
restrictScalars_smul 📖	mathematical	—	restrictScalars ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—
restrictScalars_sub 📖	mathematical	—	restrictScalars Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring sub	—	—
restrictScalars_zero 📖	mathematical	—	restrictScalars ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring zero	—	—
rightInverse_of_comp 📖	mathematical	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids id	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	RingHomCompTriple.ids leftInverse_of_comp
smulCommClass 📖	mathematical	—	SMulCommClass ContinuousLinearMap instSMul	—	ext SMulCommClass.smul_comm
smulRight_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike smulRight SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
smulRight_comp 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids smulRight Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DFunLike.coe ContinuousLinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring funLike	—	smulRight_comp_smulRight
smulRight_comp_smulRight 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids smulRight Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DFunLike.coe ContinuousLinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring funLike	—	ext RingHomCompTriple.ids IsScalarTower.left map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
smulRight_id 📖	mathematical	—	smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction id toSpanSingleton	—	IsScalarTower.left
smulRight_one_eq_iff 📖	mathematical	—	toSpanSingleton	—	—
smulRight_one_eq_toSpanSingleton 📖	mathematical	—	smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction ContinuousLinearMap RingHom.id one toSpanSingleton	—	IsScalarTower.left
smulRight_one_one 📖	mathematical	—	toSpanSingleton DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toSpanSingleton_apply_map_one
smulRight_one_pow 📖	mathematical	—	ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule Monoid.toPow MonoidWithZero.toMonoid monoidWithZero toSpanSingleton ContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Semiring.toMonoidWithZero	—	toSpanSingleton_pow
smulRight_zero 📖	mathematical	—	smulRight AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring zero	—	ext smul_zero
smul_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass	—	—
smul_comp 📖	mathematical	—	comp ContinuousLinearMap instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
smul_def 📖	mathematical	—	ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid monoidWithZero Module.toDistribMulAction semiring applyModule DFunLike.coe funLike	—	—
sub_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
sub_apply' 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.instSub toLinearMap SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ContinuousLinearMap funLike	—	—
sub_comp 📖	mathematical	—	comp Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap sub	—	ext
sum_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike Finset.sum addCommMonoid	—	coe_sum' Finset.sum_apply
toContinuousAddMonoidHom_add 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousLinearMap funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass add ContinuousAddMonoidHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ContinuousAddMonoidHom.instAddCommMonoid	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toContinuousAddMonoidHom_comp 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousLinearMap funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass comp ContinuousAddMonoidHom.comp	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toContinuousAddMonoidHom_id 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass id ContinuousAddMonoidHom.id	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toContinuousAddMonoidHom_inj 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousLinearMap funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass toContinuousAddMonoidHom_injective
toContinuousAddMonoidHom_injective 📖	mathematical	—	ContinuousLinearMap ContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousAddMonoidHom.toContinuousAddMonoidHom funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass Function.Injective.of_comp_iff DFunLike.coe_injective
toContinuousAddMonoidHom_neg 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass neg ContinuousAddMonoidHom NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousAddMonoidHom.instAddCommGroup	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toContinuousAddMonoidHom_restrictScalars 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass restrictScalars	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toContinuousAddMonoidHom_sub 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ContinuousLinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass sub ContinuousAddMonoidHom SubNegMonoid.toSub ContinuousAddMonoidHom.instAddCommGroup	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toContinuousAddMonoidHom_zero 📖	mathematical	—	ContinuousAddMonoidHom.toContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousLinearMap funLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass zero ContinuousAddMonoidHom ContinuousAddMonoidHom.instZero	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
toLinearMapRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap semiring Module.End.instSemiring RingHom.instFunLike toLinearMapRingHom toLinearMap	—	—
toLinearMap_toSpanSingleton 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule toSpanSingleton LinearMap.toSpanSingleton	—	—
toSpanSingletonLE_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike toSpanSingletonLE toSpanSingleton	—	RingHomInvPair.ids
toSpanSingletonLE_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toSpanSingletonLE funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
toSpanSingleton_add 📖	mathematical	—	toSpanSingleton AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule add	—	LinearMap.toSpanSingleton_add
toSpanSingleton_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike toSpanSingleton SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
toSpanSingleton_apply_map_one 📖	mathematical	—	toSpanSingleton DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext_ring LinearMap.IsScalarTower.compatibleSMul' IsScalarTower.left mul_one
toSpanSingleton_apply_one 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike toSpanSingleton AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	one_smul
toSpanSingleton_comp 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHomCompTriple.ids toSpanSingleton smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	RingHomCompTriple.ids
toSpanSingleton_comp_toSpanSingleton 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHomCompTriple.ids toSpanSingleton ContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smulRight_comp_smulRight ContinuousMul.to_continuousSMul
toSpanSingleton_inj 📖	mathematical	—	toSpanSingleton	—	one_smul
toSpanSingleton_one 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike toSpanSingleton AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toSpanSingleton_apply_one
toSpanSingleton_pow 📖	mathematical	—	ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule Monoid.toPow MonoidWithZero.toMonoid monoidWithZero toSpanSingleton ContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Semiring.toMonoidWithZero	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ext_ring pow_zero toSpanSingleton.congr_simp mul_one pow_succ RingHomCompTriple.ids mul_def toSpanSingleton_comp_toSpanSingleton smul_eq_mul pow_succ'
toSpanSingleton_smul 📖	mathematical	—	toSpanSingleton SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instSMul	—	LinearMap.toSpanSingleton_smul
toSpanSingleton_zero 📖	mathematical	—	toSpanSingleton AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule zero	—	ext_ring smul_zero
uniformContinuous 📖	mathematical	—	UniformContinuous DFunLike.coe ContinuousLinearMap UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid funLike	—	uniformContinuous_addMonoidHom_of_continuous DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass continuous
zero_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap funLike zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
zero_comp 📖	mathematical	—	comp ContinuousLinearMap zero	—	ext
zero_smulRight 📖	mathematical	—	smulRight ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring zero	—	ext zero_smul

ContinuousLinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commute_iff 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul	Commute ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap LinearMap.range RingHomSurjective.ids LinearMap.ker	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.IsIdempotentElem.commute_iff toLinearMap
commute_iff_of_isUnit 📖	mathematical	IsUnit ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MonoidWithZero.toMonoid ContinuousLinearMap.monoidWithZero IsIdempotentElem ContinuousLinearMap.instMul	Commute ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul Submodule.map RingHomSurjective.ids ContinuousLinearMap.toLinearMap LinearMap.range LinearMap.ker	—	IsTopologicalAddGroup.toContinuousAdd IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomSurjective.ids CanLift.prf instCanLiftUnitsValIsUnit RingHomCompTriple.ids LinearMap.IsIdempotentElem.commute_iff_of_isUnit toLinearMap
conj_eq_of_ker_mem_invtSubmodule 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap LinearMap.ker	ContinuousLinearMap.comp Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomCompTriple.ids	—	RingHomCompTriple.ids ker_mem_invtSubmodule_iff
conj_eq_of_range_mem_invtSubmodule 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap LinearMap.range RingHomSurjective.ids	ContinuousLinearMap.comp Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomCompTriple.ids	—	RingHomSurjective.ids RingHomCompTriple.ids range_mem_invtSubmodule_iff
ext 📖	—	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul LinearMap.range RingHomSurjective.ids ContinuousLinearMap.toLinearMap LinearMap.ker	—	—	RingHomSurjective.ids ext_iff
ext_iff 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul	LinearMap.range Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap LinearMap.ker	—	RingHomSurjective.ids LinearMap.IsIdempotentElem.ext_iff toLinearMap
isClosed_range 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul	IsClosed SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap	—	ContinuousLinearMap.isClosed_ker RingHomSurjective.ids LinearMap.IsIdempotentElem.range_eq_ker toLinearMap
ker_eq_range 📖	mathematical	IsIdempotentElem LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instMul	LinearMap.ker AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.range RingHomSurjective.ids LinearMap LinearMap.instSub LinearMap.id	—	LinearMap.IsIdempotentElem.ker_eq_range
ker_mem_invtSubmodule 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul ContinuousLinearMap.comp RingHomCompTriple.ids	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.ker	—	RingHomCompTriple.ids ker_mem_invtSubmodule_iff
ker_mem_invtSubmodule_iff 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.ker ContinuousLinearMap.comp RingHomCompTriple.ids	—	RingHomCompTriple.ids LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff toLinearMap
range_eq_ker 📖	mathematical	IsIdempotentElem LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instMul	LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.ker LinearMap LinearMap.instSub LinearMap.id	—	LinearMap.IsIdempotentElem.range_eq_ker
range_mem_invtSubmodule 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul ContinuousLinearMap.comp RingHomCompTriple.ids	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.range RingHomSurjective.ids	—	RingHomSurjective.ids RingHomCompTriple.ids range_mem_invtSubmodule_iff
range_mem_invtSubmodule_iff 📖	mathematical	IsIdempotentElem ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instMul	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.range RingHomSurjective.ids ContinuousLinearMap.comp RingHomCompTriple.ids	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff toLinearMap
toLinearMap 📖	mathematical	IsIdempotentElem ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.instMul	IsIdempotentElem LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMul ContinuousLinearMap.toLinearMap	—	ContinuousLinearMap.isIdempotentElem_toLinearMap_iff

ContinuousLinearMap.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

ContinuousSemilinearMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousMapClass 📖	mathematical	—	ContinuousMapClass	—	—
toSemilinearMapClass 📖	mathematical	—	SemilinearMapClass	—	—

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalClosure_map_submodule 📖	mathematical	DenseRange DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike Submodule.topologicalClosure ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Top.top Submodule Submodule.instTop	Submodule.topologicalClosure ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Submodule.map ContinuousLinearMap.toLinearMap Top.top Submodule Submodule.instTop	—	ContinuousSMul.continuousConstSMul SetLike.ext'_iff dense_image ContinuousLinearMap.continuous

Submodule

Definitions

Name	Category	Theorems
ClosedComplemented 📖	MathDef	10 math math: closedComplemented_top, ContinuousLinearMap.closedComplemented_ker_of_rightInverse, closedComplemented_bot, IsCompl.closedComplemented_of_isClosed, ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range, ClosedComplemented.of_finiteDimensional, ContinuousLinearMap.HasLeftInverse.closedComplemented_range, closedComplemented_iff_isClosed_exists_isClosed_isCompl, ClosedComplemented.of_quotient_finiteDimensional, ClosedComplemented.of_isCompl_isClosed
subtypeL 📖	CompOp	19 math math: subtypeₗᵢ_toContinuousLinearMap, coe_subtypeL', IsOrtho.orthogonalProjection_comp_subtypeL, coe_orthogonalDecomposition_symm, HasStrictFDerivAt.to_implicitFunctionOfComplemented, adjoint_subtypeL, range_subtypeL, norm_subtypeL, HasStrictFDerivAt.to_implicitFunction, ker_subtypeL, subtypeL_apply, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, adjoint_orthogonalProjection, ContinuousLinearMap.exist_extension_of_finiteDimensional_range, orthogonalProjection_comp_subtypeL_eq_zero_iff, norm_subtypeL_le, coe_subtypeL, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, hasFDerivAt_stereoInvFunAux_comp_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedComplemented_bot 📖	mathematical	—	ClosedComplemented Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instBot	—	eq_zero_of_bot_submodule
closedComplemented_top 📖	mathematical	—	ClosedComplemented Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instTop	—	—
coe_subtypeL 📖	mathematical	—	ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module subtypeL subtype	—	—
coe_subtypeL' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike subtypeL LinearMap LinearMap.instFunLike subtype	—	—
ker_subtypeL 📖	mathematical	—	LinearMap.ker Submodule SetLike.instMembership setLike addCommMonoid module RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toLinearMap instTopologicalSpaceSubtype subtypeL Bot.bot instBot	—	ker_subtype
range_subtypeL 📖	mathematical	—	LinearMap.range Submodule SetLike.instMembership setLike addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap instTopologicalSpaceSubtype subtypeL	—	range_subtype
subtypeL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike subtypeL	—	—
topologicalClosure_map 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder map ContinuousLinearMap.toLinearMap topologicalClosure ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	image_closure_subset_closure_image ContinuousLinearMap.continuous
topologicalClosure_mem_invtSubmodule 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring topologicalClosure ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ContinuousSMul.continuousConstSMul RingHomSurjective.ids Module.End.mem_invtSubmodule_iff_map_le LE.le.trans topologicalClosure_map topologicalClosure_mono

Submodule.ClosedComplemented

Definitions

Name	Category	Theorems
complement 📖	CompOp	2 math math: isClosed_complement, isCompl_complement

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isClosed_isCompl 📖	mathematical	Submodule.ClosedComplemented	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid IsClosed SetLike.coe Submodule.setLike IsCompl Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice	—	ContinuousLinearMap.isClosed_ker LinearMap.isCompl_of_proj
isClosed 📖	mathematical	Submodule.ClosedComplemented	IsClosed SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike	—	RingHomCompTriple.ids LinearMap.ker_id_sub_eq_of_proj ContinuousLinearMap.isClosed_ker
isClosed_complement 📖	mathematical	Submodule.ClosedComplemented	IsClosed SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike complement	—	exists_isClosed_isCompl
isCompl_complement 📖	mathematical	Submodule.ClosedComplemented	IsCompl Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice complement	—	exists_isClosed_isCompl

(root)

Definitions

Name	Category	Theorems
ContinuousLinearMapClass 📖	MathDef	5 math math: LinearMap.continuousLinearMapClassOfFiniteDimensional, PositiveLinearMap.instContinuousLinearMapClassComplexOfLinearMapClassOfOrderHomClass, AlgHom.instContinuousLinearMapClassOfAlgHomClass, NonUnitalStarAlgHom.instContinuousLinearMapClassComplex, WeakDual.CharacterSpace.instContinuousLinearMapClass
ContinuousSemilinearMapClass 📖	CompData	5 math math: ContinuousSemilinearEquivClass.continuousSemilinearMapClass, SemilinearIsometryClass.toContinuousSemilinearMapClass, ContinuousLinearMap.continuousSemilinearMapClass, UniformConvergenceCLM.instContinuousSemilinearMapClass, ContinuousLinearMapWOT.instContinuousLinearMapClass
StrongDual 📖	CompOp	316 math math: geometric_hahn_banach_open, HasStrictFDerivAt.log, NormedSpace.isBounded_polar_of_mem_nhds_zero, HasFDerivWithinAt.ccosh, RCLike.geometric_hahn_banach_point_open, HasFDerivWithinAt.ccos, InnerProductSpace.toLinearIsometry_toDual, geometric_hahn_banach_point_point, hasFDerivAt_iff_hasGradientAt, RCLike.reCLM_apply, RCLike.separate_convex_open_set, StrongDual.norm_extendRCLike, HasStrictFDerivAt.csin, ContinuousLinearMap.opNorm_bound_of_ball_bound, NormedSpace.Dual.isClosed_image_polar_of_mem_nhds, ProbabilityTheory.covarianceBilinDual_apply', MeasureTheory.charFunDual_apply, ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq, IsLocalMaxOn.hasFDerivWithinAt_nonpos, ProbabilityTheory.IsGaussian.integrable_dual, geometric_hahn_banach_open_point, StrongDual.polarSubmodule_eq_setOf, ContinuousLinearMapWOT.withSeminorms, ProbabilityTheory.covarianceBilinDual_apply, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, ProbabilityTheory.IndepFun.charFunDual_map_fun_add_eq_mul, RCLike.geometric_hahn_banach_of_nonempty_interior_point, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, ProbabilityTheory.uncenteredCovarianceBilin_apply, StrongDual.norm_extendRCLike_bound, LipschitzWith.ae_exists_fderiv_of_countable, InnerProductSpace.toDual_symm_apply, MeasureTheory.charFun_toDual_symm_eq_charFunDual, GeneralSchauderBasis.proj_apply, exposed_point_def, ContinuousLinearMap.norm_extendTo𝕜, geometric_hahn_banach_compact_closed, HasFDerivWithinAt.csin, ProbabilityTheory.iIndepFun.charFunDual_map_finset_sum_eq_prod, NormedSpace.Dual.toWeakDual_continuous, RCLike.reCLM_norm, RCLike.geometric_hahn_banach_closed_point, ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod, SeparatingDual.exists_eq_one, NormedSpace.isClosed_polar, MeasureTheory.charFunDual_eq_charFun_map_one, ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds, HasFDerivAt.arctan, HasStrictFDerivAt.abs, HasStrictFDerivAt.arsinh, HasFDerivWithinAt.exp, ContinuousLinearMapWOT.inducingFn_apply, RCLike.iInter_countable_halfSpaces_eq, InnerProductSpace.toDualMap_apply_apply, HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg, WeakDual.toStrongDual_inj, LinearMap.dualEmbedding_surjective, StrongDual.toWeakDual_inj, WeakDual.coe_toStrongDual, NormedSpace.eq_zero_iff_forall_dual_eq_zero, geometric_hahn_banach_of_nonempty_interior_point, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, hasGradientWithinAt_iff_hasFDerivWithinAt, NormedSpace.smul_mem_polar, GeneralSchauderBasis.expansion, NormedSpace.inclusionInDoubleDual_norm_eq, tendsto_integral_exp_smul_cocompact, HasFDerivWithinAt.abs_of_neg, LinearMap.toLinearMap_toContPerfPair, ContinuousLinearMap.norm_smulRightL, NormedSpace.inclusionInDoubleDualWeak_apply_apply, NormedSpace.eq_iff_forall_dual_eq, NormedSpace.toLinearMap_inclusionInDoubleDualWeak, HasFDerivWithinAt.hasGradientWithinAt, HasFDerivWithinAt.cpow, StrongDual.toLp_of_not_memLp, HasStrictFDerivAt.const_cpow, HasFDerivWithinAt.csinh, NormedSpace.inclusionInDoubleDual_norm_le, HasFDerivAt.abs, WeakDual.isCompact_closedBall, HasStrictFDerivAt.abs_of_neg, HasFDerivWithinAt.abs, InnerProductSpace.toDual_apply, ProbabilityTheory.covarianceBilinDual_eq_covariance, EuclideanSpace.coe_proj, ProbabilityTheory.covarianceBilinDual_zero, NormedSpace.polar_ball_subset_closedBall_div, InnerProductSpace.toDualMap_apply, geometric_hahn_banach_point_closed, HasStrictFDerivAt.clog, HasStrictFDerivAt.sqrt, RCLike.geometric_hahn_banach_of_nonempty_interior', HasStrictFDerivAt.rpow, InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjointAux_apply, IsLocalMinOn.hasFDerivWithinAt_nonneg, ContinuousLinearMap.norm_smulRight_apply, ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero, HasStrictFDerivAt.ccos, ContinuousLinearMapWOT.isInducing_inducingFn, StrongDual.polarSubmodule_eq_polar, RCLike.geometric_hahn_banach_point_point, SchauderBasis.proj_apply, ContinuousLinearMapWOT.hasBasis_seminorms, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, IsLocalMinOn.hasFDerivWithinAt_eq_zero, ProperCone.hyperplane_separation_point, IsLocalMax.hasFDerivAt_eq_zero, WeakDual.isSeqCompact_closedBall, HasFDerivAt.ccos, HasFDerivWithinAt.log, HasFDerivAt.clog, BoundedContinuousFunction.probCharDual_zero, HasGradientAt.hasFDerivAt, ContinuousLinearMapWOT.isEmbedding_inducingFn, geometric_hahn_banach_of_nonempty_interior', ProperCone.dual_singleton, StrongDual.extendRCLikeₗ_apply, NormedSpace.inclusionInDoubleDualWeak_apply, HasFDerivAt.ccosh, exists_dual_vector, HasFDerivAt.abs_of_neg, ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, SeparatingDual.eq_zero_iff_forall_dual_eq_zero, HasStrictFDerivAt.arctan, LinearPMap.adjointDomainMkCLM_apply, iInter_halfSpaces_eq, geometric_hahn_banach_closed_compact, ProbabilityTheory.iIndepFun.charFunDual_map_sum_eq_prod, ProbabilityTheory.covarianceBilinDual_self_eq_variance, geometric_hahn_banach_open_open, tendsto_integral_exp_smul_cocompact_of_inner_product, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, HasFDerivWithinAt.sinh, exists_dual_vector'', ProbabilityTheory.IsGaussian.memLp_dual, ProbabilityTheory.covarianceBilinDual_self_nonneg, HasFDerivAt.log, MeasureTheory.charFunDual_map_const_add, MeasureTheory.charFunDual_map_add_const, HasFDerivAt.exp, ContinuousLinearMap.norm_extendTo𝕜'_bound, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d, WeakDual.isClosed_closedBall, StrongDual.extendRCLikeₗᵢ_symm_apply, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, ProbabilityTheory.integral_strongDual_stdGaussian, StrongDual.toLpₗ_apply, StrongDual.extendRCLikeₗ_symm_apply, HasFDerivWithinAt.rpow_const, IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, ContinuousLinearMap.extendTo𝕜_apply, HasFDerivAt.sinh, ProbabilityTheory.IsGaussian.integral_dual, ContinuousLinearMap.norm_extendTo𝕜', StrongDual.polar_univ, HasFDerivWithinAt.clog, hasGradientAt_iff_hasFDerivAt, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, ProbabilityTheory.variance_dual_stdGaussian, HasFDerivAt.rpow_const, coord_norm', ContinuousLinearMapWOT.ext_dual_iff, StrongDual.extendRCLikeₗᵢ_apply, HasStrictFDerivAt.const_rpow, StrongDual.norm_toLpₗ_le, WeakDual.isBounded_toWeakDual_preimage_iff_isBounded, HasStrictFDerivAt.cos, HasFDerivWithinAt.arsinh, geometric_hahn_banach_point_open, StrongDual.toLpₗ_of_not_memLp, StrongDual.mem_polarSubmodule, exists_dual_vector', MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, separate_convex_open_set, RCLike.geometric_hahn_banach_open, HasFDerivAt.sin, HasFDerivAt.csin, WStarAlgebra.exists_predual, GeneralSchauderBasis.ortho, IsExposed.eq_inter_halfSpace, ProbabilityTheory.isPosSemidef_covarianceBilinDual, SeparatingDual.exists_ne_zero, HasFDerivAt.hasFDerivAt_norm_smul, ProbabilityTheory.charFunDual_map_sum_pi_eq_prod, AlgHom.coe_toContinuousLinearMap, HasFDerivWithinAt.sqrt, SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair, NormedSpace.polar_ball, InnerProductSpace.toContinuousLinearMap_toDualMap, SeparatingDual.exists_ne_zero', HasFDerivWithinAt.const_cpow, WeakDual.CharacterSpace.norm_le_norm_one, InnerProductSpace.toDual_apply_eq_toDualMap_apply, ProbabilityTheory.variance_dual_prod', HasFDerivWithinAt.arctan, ProbabilityTheory.covarianceBilinDual_comm, ProbabilityTheory.isGaussian_iff_charFunDual_eq, NormedSpace.isEmbedding_inclusionInDoubleDualWeak, HasFDerivWithinAt.rpow, MeasureTheory.charFun_eq_charFunDual_toDualMap, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology, NormedSpace.sInter_polar_eq_closedBall, HasFDerivAt.cos, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, HasFDerivAt.const_rpow, ContinuousLinearMap.nnnorm_smulRight_apply, ProbabilityTheory.charFunDual_map_add_prod_eq_mul, HasFDerivAt.arsinh, StrongDual.zero_mem_polar, ContinuousLinearMapWOT.continuous_inducingFn, LinearPMap.adjointDomainMkCLMExtend_apply, HasStrictFDerivAt.cpow, hasFDerivWithinAt_iff_hasGradientWithinAt, StrongDual.extendRCLike_apply, ProbabilityTheory.uncenteredCovarianceBilin_zero, LinearMap.toContPerfPair_apply, OrthonormalBasis.norm_dual, MeasureTheory.charFunDual_dirac, WeakDual.isBounded_toStrongDual_preimage_iff_isBounded, StrongDual.toWeakDual_apply, AlgHom.toContinuousLinearMap_norm, HasFDerivAt.hasFDerivAt_norm_smul_neg, StrongDual.toLp_apply, StrongDual.polar_empty, IsLocalMin.hasFDerivAt_eq_zero, ProbabilityTheory.iIndepFun.charFunDual_map_fun_finset_sum_eq_prod, exists_extension_norm_eq, separatingDual_def, NormedSpace.closedBall_inv_subset_polar_closedBall, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, ContinuousLinearMap.norm_smulRightL_le, StrongDual.im_extendRCLike_apply, WeakDual.isBounded_closedBall, ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero, ProbabilityTheory.variance_dual_prod, HasFDerivAt.hasGradientAt, HasStrictFDerivAt.sin, HasFDerivWithinAt.const_rpow, RCLike.geometric_hahn_banach_of_nonempty_interior, ContinuousLinearMap.extendTo𝕜'_apply, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, RCLike.re_extendTo𝕜ₗ, ContinuousLinearEquiv.coord_norm', LinearMap.dualEmbedding_injective_of_separatingRight, StrongDual.re_extendRCLike_apply, IsLocalMaxOn.hasFDerivWithinAt_eq_zero, StrongDual.coe_toWeakDual, WeakDual.toStrongDual_apply, geometric_hahn_banach_closed_point, SeparatingDual.exists_separating_of_ne, RCLike.iInter_halfSpaces_eq', HasFDerivAt.sqrt, HasFDerivAt.csinh, RCLike.iInter_halfSpaces_eq, StrongDual.polar_zero, ProperCone.hyperplane_separation, StrongDual.mem_polar_iff, ContinuousLinearEquiv.coord_self, RCLike.geometric_hahn_banach_compact_closed, HasStrictFDerivAt.ccosh, ContinuousLinearEquiv.coord_norm, HasStrictFDerivAt.cosh, RCLike.geometric_hahn_banach_point_closed, NormedSpace.polar_closedBall, IsExposed.eq_inter_halfSpace', ProbabilityTheory.covarianceBilinDual_of_not_memLp, MeasureTheory.charFun_map_eq_charFunDual_smul, NormedSpace.double_dual_bound, Real.zero_at_infty_vector_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, HasStrictFDerivAt.sinh, HasFDerivAt.cpow, ProbabilityTheory.IsGaussian.charFunDual_eq', StrongDual.polar_singleton, HasFDerivAt.cosh, ContinuousLinearMap.isOpenMap_of_ne_zero, ContinuousLinearMapWOT.continuous_dual_apply, StrongDual.mem_polar_singleton, HasStrictFDerivAt.csinh, HasFDerivWithinAt.cos, Real.exists_extension_norm_eq, ProbabilityTheory.covarianceBilinDual_of_not_memLp', HasGradientWithinAt.hasFDerivWithinAt, ContinuousLinearMap.smulRightL_apply_apply, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, IsLocalExtr.hasFDerivAt_eq_zero, RCLike.geometric_hahn_banach_closed_compact, ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, HasFDerivAt.rpow, ContinuousLinearMap.norm_smulRightL_apply, HasFDerivWithinAt.sin, HasStrictFDerivAt.exp, RCLike.imCLM_apply, domain_mvt, StrongDual.polar_nonempty, NormedSpace.dual_def, RCLike.geometric_hahn_banach_open_open, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, ProbabilityTheory.charFunDual_stdGaussian, geometric_hahn_banach_of_nonempty_interior, SeparatingDual.eq_iff_forall_dual_eq, BoundedContinuousFunction.probCharDual_apply, HasFDerivAt.const_cpow, HasFDerivWithinAt.cosh, HasStrictFDerivAt.rpow_const, RCLike.geometric_hahn_banach_open_point
topDualPairing 📖	CompOp	5 math math: topDualPairing_isContPerfPair, StrongDual.dualPairing_separatingLeft, tendsto_iff_forall_eval_tendsto_topDualPairing, topDualPairing_apply, Real.zero_at_infty_vector_fourierIntegral
«term_→L[_]_» 📖	CompOp	—
«term_→SL[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topDualPairing_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike ContinuousLinearMap ContinuousLinearMap.addCommMonoid LinearMap.addCommMonoid ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.module topDualPairing ContinuousLinearMap.funLike	—	Algebra.to_smulCommClass

---

← Back to Index