Basic

📁 Source: Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

Statistics

Metric	Count
Definitions compContinuousMultilinearMap, apply, addCommMonoid, applyAddHom, codRestrict, compContinuousLinearMap, constOfIsEmpty, domDomCongr, domDomCongrEquiv, funLike, instAdd, instAddCommGroup, instDistribMulAction, instInhabited, instModule, instMulAction, instNeg, instSMul, instSub, instZero, linearDeriv, mkPiAlgebra, mkPiAlgebraFin, mkPiRing, ofSubsingleton, pi, piEquiv, piLinearEquiv, prod, prodEquiv, restrictScalars, smulRight, toContinuousLinearMap, toMultilinearMap, toMultilinearMapLinear, «term_[×_]→L[_]_»	36
Theorems compContinuousMultilinearMap_coe, add_apply, add_prod_add, codRestrict_apply_coe, codRestrict_toMultilinearMap, coe_coe, coe_continuous, coe_pi, coe_restrictScalars, compContinuousLinearMap_apply, cons_add, cons_smul, constOfIsEmpty_apply, constOfIsEmpty_toMultilinearMap, cont, continuousMapClass, domDomCongrEquiv_apply, domDomCongrEquiv_symm_apply, domDomCongr_apply, domDomCongr_toMultilinearMap, eq_prod_iff, ext, ext_iff, ext_ring, ext_ring_iff, instIsCentralScalar, instIsScalarTower, instSMulCommClass, linearDeriv_apply, map_add_univ, map_coord_zero, map_piecewise_add, map_piecewise_smul, map_smul_univ, map_sum, map_sum_finset, map_update_add, map_update_smul, map_update_sub, map_zero, mkPiAlgebraFin_apply, mkPiAlgebra_apply, mkPiAlgebra_eq_mkPiAlgebraFin, mkPiRing_apply, mkPiRing_apply_one_eq_self, mkPiRing_eq_iff, mkPiRing_eq_zero_iff, mkPiRing_zero, neg_apply, neg_prod_neg, ofSubsingleton_apply_apply, ofSubsingleton_apply_toMultilinearMap, ofSubsingleton_symm_apply_apply, piEquiv_apply, piEquiv_symm_apply, piLinearEquiv_apply, piLinearEquiv_symm_apply, pi_apply, prodEquiv_apply, prodEquiv_symm_apply, prodEquiv_symm_apply_fst, prodEquiv_symm_apply_snd, prod_apply, prod_ext, prod_ext_iff, smulRight_apply, smulRight_toMultilinearMap, smul_apply, smul_prod_smul, sub_apply, sub_prod_sub, sum_apply, toContinuousLinearMap_apply, toMultilinearMapLinear_apply, toMultilinearMap_add, toMultilinearMap_injective, toMultilinearMap_smul, toMultilinearMap_zero, zero_apply, zero_prod_zero	80
Total	116

ContinuousLinearMap

Definitions

Name	Category	Theorems
compContinuousMultilinearMap 📖	CompOp	25 math math: norm_compContinuousMultilinearMap_le, ContinuousMultilinearMap.eq_prod_iff, ContinuousMultilinearMap.piLinearEquiv_symm_apply, ContinuousMultilinearMap.prod_ext_iff, isBoundedBilinearMap_compMultilinear, LinearIsometry.norm_compContinuousMultilinearMap, iteratedFDerivWithin_smul_const_apply, hasFTaylorSeriesUpToOn_pi', ContinuousMultilinearMap.prodEquiv_symm_apply_fst, iteratedFDerivWithin_comp_left, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, compFormalMultilinearSeries_apply, ContinuousMultilinearMap.prodEquiv_symm_apply, compContinuousMultilinearMap_coe, ContinuousMultilinearMap.prodEquiv_symm_apply_snd, ContinuousLinearEquiv.iteratedFDeriv_comp_left, iteratedFDeriv_smul_const_apply, PiTensorProduct.liftIsometry_symm_apply, ContinuousMultilinearMap.piₗᵢ_symm_apply, ContinuousMultilinearMap.piEquiv_symm_apply, ContinuousMultilinearMap.isUniformInducing_postcomp, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply, FormalMultilinearSeries.rightInv_coeff, iteratedFDeriv_comp_left, ContinuousLinearEquiv.iteratedFDerivWithin_comp_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compContinuousMultilinearMap_coe 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike compContinuousMultilinearMap ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	—

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
addCommMonoid 📖	CompOp	136 math math: fderiv_iteratedFDeriv, HasFDerivWithinAt.continuousMultilinearMap_apply, FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite, norm_iteratedFDerivComponent_le, ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, FormalMultilinearSeries.changeOriginSeriesTerm_apply, alternatization_apply_apply, ContDiffMapSupportedIn.structureMapCLM_apply, MultilinearMap.mkContinuousMultilinear_apply, norm_compContinuousLinearMapLRight_le, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, piLinearEquiv_symm_apply, HasFDerivWithinAt.linear_multilinear_comp, iteratedFDerivWithin_succ_eq_comp_left, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, norm_smulRightL_le, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, VectorFourier.fourierPowSMulRight_eq_comp, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, ContinuousLinearMap.flipMultilinear_apply_apply, uncurrySum_apply, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, curryFinFinset_symm_apply_const, curryLeft_norm, ContDiffMapSupportedIn.structureMapLM_eq_of_scalars, restrictScalarsLinear_apply, ContDiffMapSupportedIn.uniformSpace_eq_iInf, ContDiffMapSupportedIn.continuous_iff_comp_withOrder, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, FormalMultilinearSeries.iteratedFDerivSeries_eq_zero, ContDiffMapSupportedIn.structureMapCLM_zero_apply, sum_apply, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, iteratedFDeriv_tsum, ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear, OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply, prodL_apply, ContinuousLinearMap.coe_flipMultilinearEquiv, PiTensorProduct.liftEquiv_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, PiTensorProduct.liftEquiv_apply, fderivWithin_iteratedFDerivWithin, MultilinearMap.mkContinuousLinear_norm_le, piLinearEquiv_apply, ContinuousLinearMap.uncurryLeft_apply, curryFinFinset_apply_const, compContinuousLinearMapLRight_apply, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, apply_apply, flipLinear_apply_apply, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, ContinuousAlternatingMap.toContinuousMultilinearMapLinear_apply, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, PiTensorProduct.dualSeminorms_bounded, curryMidEquiv_apply, ContinuousLinearMap.norm_map_tail_le, PiTensorProduct.injectiveSeminorm_apply, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, MultilinearMap.mkContinuousLinear_norm_le', ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, ContinuousLinearMap.continuous_uncurry_of_multilinear, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, MultilinearMap.mkContinuousMultilinear_norm_le', curryFinFinset_symm_apply_piecewise_const, ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, ContinuousLinearMap.uncurryMid_apply, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, continuousMultilinearCurryLeftEquiv_apply, alternatization_apply_toContinuousMultilinearMap, iteratedFDerivComponent_apply, changeOriginSeries_support, ContDiffMapSupportedIn.seminorm_apply, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, piₗᵢ_symm_apply, fderiv_continuousMultilinearMapCompContinuousLinearMap, MultilinearMap.mkContinuousMultilinear_norm_le, hasStrictFDerivAt_compContinuousLinearMap, curryMid_apply, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply, compContinuousLinearMapL_apply, prodL_symm_apply, alternatization_apply_toAlternatingMap, ContDiffMapSupportedIn.structureMapLM_zero_injective, curryLeft_apply, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, currySum_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply, FormalMultilinearSeries.changeOriginSeries_finite_of_finite, ContDiffMapSupportedIn.continuous_iff_comp, continuousMultilinearCurryLeftEquiv_symm_apply, smulRightL_apply, iteratedFDeriv_succ_eq_comp_left, ContDiffMapSupportedIn.structureMapCLM_zero_injective, piₗᵢ_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm, FormalMultilinearSeries.norm_changeOriginSeriesTerm, fderivCompContinuousLinearMap_apply, curryFinFinset_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm, FormalMultilinearSeries.rightInv_coeff, norm_compContinuousLinearMapL_le, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, ContDiffMapSupportedIn.structureMapLM_zero_apply, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, iteratedFDeriv_tsum_apply, toMultilinearMapLinear_apply, HasStrictFDerivAt.continuousMultilinearMap_apply, curryFinFinset_apply, FormalMultilinearSeries.changeOriginSeriesTerm_bound, ContinuousLinearMap.norm_map_removeNth_le, hasStrictFDerivAt_uncurry, compContinuousLinearMapContinuousMultilinear_apply_apply, ContDiffMapSupportedIn.structureMapLM_apply, isBoundedLinearMap_prod_multilinear, norm_curryMid, ContinuousAlternatingMap.toMultilinearAddHom_apply, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, curryMidEquiv_symm_apply, HasFDerivAt.continuousMultilinearMap_apply
applyAddHom 📖	CompOp	—
codRestrict 📖	CompOp	2 math math: codRestrict_apply_coe, codRestrict_toMultilinearMap
compContinuousLinearMap 📖	CompOp	33 math math: analyticAt_uncurry_compContinuousLinearMap, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFTaylorSeriesUpToOn.comp_continuousAffineMap, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, norm_compContinuous_linearIsometry_le, ContinuousLinearEquiv.iteratedFDerivWithin_comp_right, ContinuousLinearMap.iteratedFDerivWithin_comp_right, DifferentiableAt.continuousMultilinearMapCompContinuousLinearMap, compContinuousLinearMapLRight_apply, Differentiable.continuousMultilinearMapCompContinuousLinearMap, compContinuousLinearMap_apply, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, HasFTaylorSeriesUpToOn.compContinuousLinearMap, DifferentiableOn.continuousMultilinearMapCompContinuousLinearMap, PiTensorProduct.mapLMultilinear_apply_apply, PiTensorProduct.liftIsometry_comp_mapL, fderiv_continuousMultilinearMapCompContinuousLinearMap, hasStrictFDerivAt_compContinuousLinearMap, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply, compContinuousLinearMapL_apply, cpolynomialOn_uncurry_compContinuousLinearMap, analyticWithinAt_uncurry_compContinuousLinearMap, norm_compContinuous_linearIsometryEquiv, analyticOnNhd_uncurry_compContinuousLinearMap, cpolynomialAt_uncurry_compContinuousLinearMap, ContinuousLinearMap.iteratedFDeriv_comp_right, isBoundedLinearMap_continuousMultilinearMap_comp_linear, analyticOn_uncurry_compContinuousLinearMap, norm_compContinuousLinearMap_le, compContinuousLinearMapContinuousMultilinear_apply_apply, DifferentiableWithinAt.continuousMultilinearMapCompContinuousLinearMap, PiTensorProduct.mapLMultilinear_toFun_apply
constOfIsEmpty 📖	CompOp	5 math math: nnnorm_constOfIsEmpty, constOfIsEmpty_toMultilinearMap, constOfIsEmpty_apply, ContinuousAlternatingMap.constOfIsEmpty_toContinuousMultilinearMap, norm_constOfIsEmpty
domDomCongr 📖	CompOp	12 math math: AnalyticOn.domDomCongr_iteratedFDerivWithin, domDomCongr_toMultilinearMap, isSymmSndFDerivAt_iff_iteratedFDeriv, AnalyticOn.domDomCongr_iteratedFDeriv, ContDiffWithinAt.domDomCongr_iteratedFDerivWithin, domDomCongr_apply, ContDiffAt.domDomCongr_iteratedFDeriv, alternatization_apply_toContinuousMultilinearMap, norm_domDomCongr, domDomCongrEquiv_apply, isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin, domDomCongrEquiv_symm_apply
domDomCongrEquiv 📖	CompOp	2 math math: domDomCongrEquiv_apply, domDomCongrEquiv_symm_apply
funLike 📖	CompOp	316 math math: map_piecewise_smul, FormalMultilinearSeries.comp_rightInv_aux1, HasFDerivWithinAt.continuousMultilinearMap_apply, FormalMultilinearSeries.comp_partialSum, cpolynomialOn, FormalMultilinearSeries.ofScalars_apply_eq', map_smul_univ, NormedSpace.expSeries_summable_of_mem_ball, norm_iteratedFDerivComponent_le, le_mul_prod_of_opNorm_le_of_le, HasFPowerSeriesWithinOnBall.hasSum_sub, analyticAt_uncurry_of_linear, norm_map_snoc_le, Differentiable.continuousMultilinear_apply_const, FormalMultilinearSeries.changeOriginSeriesTerm_apply, alternatization_apply_apply, map_update_sub, FormalMultilinearSeries.congr, coe_coe, iteratedDerivWithin_vcomp_two, mkPiAlgebra_apply, bilinearIteratedFDerivTwo_eq_iteratedFDeriv, MultilinearMap.mkContinuousMultilinear_apply, uniformContinuous_eval_const, HasFPowerSeriesAt.eventually_hasSum, FormalMultilinearSeries.hasSum_of_finite, contDiffAt, HasFDerivWithinAt.linear_multilinear_comp, mkPiRing_apply_one_eq_self, mkPiRing_apply, HasFDerivAt.continuousMultilinear_apply_const, AnalyticOn.iteratedFDerivWithin_comp_perm, FormalMultilinearSeries.ofScalars_apply_eq, HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, FormalMultilinearSeries.id_apply_one', tensorIteratedFDerivTwo_eq_iteratedFDeriv, HasFPowerSeriesOnBall.hasSum_iteratedFDeriv, curry0_apply, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, HasFDerivAt.multilinear_comp, linearDeriv_apply, NormedSpace.expSeries_apply_eq_div', Real.fourierIntegral_continuousMultilinearMap_apply, Bornology.IsVonNBounded.image_multilinear', iteratedDerivWithin_eq_iteratedFDerivWithin, VectorFourier.fourierPowSMulRight_eq_comp, le_of_opNNNorm_le, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, ContinuousLinearMap.flipMultilinear_apply_apply, uncurrySum_apply, map_sum, NormedSpace.expSeries_eq_expSeries, NormedSpace.expSeries_summable, FormalMultilinearSeries.comp_coeff_zero, FormalMultilinearSeries.ofScalars_apply_zero, ext_ring_iff, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, TrivSqZeroExt.fst_expSeries, mkPiAlgebraFin_apply, unit_le_opNorm, cauchyPowerSeries_apply, HasFPowerSeriesOnBall.coeff_zero, tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin, norm_image_sub_le, NormedSpace.norm_expSeries_summable, MultilinearMap.coe_mkContinuous, map_update_add, curryFinFinset_symm_apply_const, neg_apply, PiTensorProduct.tprodL_toFun, iteratedFDerivWithin_succ_apply_right, le_opNorm, NormedSpace.expSeries_hasSum_exp, FormalMultilinearSeries.hasSum, ContinuousLinearMap.compFormalMultilinearSeries_apply', fderivWithin_continuousMultilinear_apply_const_apply, Quaternion.expSeries_odd_of_imaginary, HasFPowerSeriesWithinAt.coeff_zero, cons_smul, ofSubsingleton_symm_apply_apply, hasFTaylorSeriesUpTo_iteratedFDeriv, map_piecewise_add, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, ordinaryHypergeometricSeries_apply_eq', sum_apply, Bornology.IsVonNBounded.image_multilinear, hasBasis_nhds_zero, compContinuousLinearMap_zero, FormalMultilinearSeries.apply_eq_pow_smul_coeff, fderivWithin_continuousMultilinear_apply_const, continuousMultilinearCurryFin0_symm_apply, FormalMultilinearSeries.compAlongComposition_bound, continuousMultilinearCurryRightEquiv_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, constOfIsEmpty_apply, ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear, hasFiniteFPowerSeriesOnBall, analyticAt, norm_map_init_le, ordinaryHypergeometricSeries_apply_zero, NormedSpace.norm_expSeries_summable_of_mem_ball, binomialSeries_apply, cons_add, map_add_univ, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, iteratedFDerivWithin_one_apply, cpolyomialOn_uncurry_of_linear, hasSum_cauchyPowerSeries_integral, HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt, HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub, coe_continuous, HasFPowerSeriesOnBall.hasSum, NormedSpace.expSeries_apply_eq, instContinuousEvalConstForall, contDiff, ContinuousLinearMap.uncurryLeft_apply, HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le, curryFinFinset_apply_const, compContinuousLinearMapLRight_apply, HasFPowerSeriesAt.hasStrictDerivAt, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, apply_apply, flipLinear_apply_apply, hasStrictFDerivAt, pi_apply, toContinuousLinearMap_apply, ContinuousLinearMap.uncurryBilinear_apply, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, Quaternion.expSeries_even_of_imaginary, NormedSpace.expSeries_apply_eq_div, tsum_eval, HasFPowerSeriesAt.apply_eq_zero, FormalMultilinearSeries.comp_coeff_one, iteratedDeriv_vcomp_three, iteratedFDerivWithin_two_apply', ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, FormalMultilinearSeries.applyComposition_single, continuousMultilinearCurryFin0_apply, iteratedFDeriv_eq, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, HasStrictFDerivAt.continuousMultilinear_apply_const, NormedSpace.expSeries_apply_zero, iteratedFDerivWithin_succ_apply_left, DifferentiableOn.continuousMultilinear_apply_const, cpolynomialAt_uncurry_of_linear, instContinuousEval, compContinuousLinearMap_apply, FormalMultilinearSeries.id_comp, ContinuousLinearMap.norm_map_tail_le, map_coord_zero, ContinuousLinearMap.compContinuousMultilinearMap_coe, iteratedFDeriv_comp_diagonal, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, ordinaryHypergeometricSeries_apply_eq, hasSum_eval, HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp, uncurryRight_apply, cpolynomialAt, ratio_le_opNorm, integral_apply, iteratedFDeriv_zero_apply, HasFDerivWithinAt.multilinear_comp, fderiv_continuousMultilinear_apply_const_apply, add_apply, ContinuousLinearMap.continuous_uncurry_of_multilinear, curryRight_apply, NormedSpace.expSeries_apply_eq', curryFinFinset_symm_apply_piecewise_const, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, AnalyticOn.iteratedFDeriv_comp_perm, domDomCongr_apply, analyticOn_uncurry_of_linear, iteratedFDeriv_one_apply, HasFPowerSeriesOnBall.factorial_smul, iteratedFDeriv_succ_apply_right, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, FormalMultilinearSeries.comp_coeff_zero', smul_apply, HasFPowerSeriesOnBall.eventually_hasSum, IsSymmSndFDerivAt.iteratedFDeriv_cons, FormalMultilinearSeries.id_apply_zero, PiTensorProduct.mapLMultilinear_apply_apply, ContinuousLinearMap.uncurryMid_apply, HasFPowerSeriesWithinOnBall.coeff_zero, norm_iteratedFDeriv_le, DifferentiableAt.continuousMultilinear_apply_const, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, ContinuousAlternatingMap.coe_mk, FormalMultilinearSeries.apply_eq_prod_smul_coeff, HasFDerivWithinAt.continuousMultilinear_apply_const, le_opNorm_mul_pow_card_of_le, continuousMultilinearCurryLeftEquiv_apply, HasFPowerSeriesAt.deriv, iteratedFDerivComponent_apply, SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv, hasFDerivAt, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv, hasBasis_nhds_zero_of_basis, uniformContinuous_coe_fun, SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv, OrderedFinpartition.compAlongOrderFinpartition_apply, ContDiffAt.iteratedFDeriv_comp_perm, HasFPowerSeriesAt.eventually_hasSum_of_comp, sub_apply, coe_pi, fderiv_continuousMultilinear_apply_const, OrderedFinpartition.applyOrderedFinpartition_apply, analyticOn, curryMid_apply, iteratedDeriv_eq_iteratedFDeriv, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, map_update_smul, PiTensorProduct.tprodL_apply, HasFPowerSeriesAt.hasDerivAt, HasFPowerSeriesAt.eventually_hasSum_sub, HasFDerivAt.linear_multilinear_comp, FormalMultilinearSeries.compAlongComposition_apply, le_opNorm_mul_prod_of_le, analyticOnNhd, analyticWithinAt_uncurry_of_linear, HasFPowerSeriesOnBall.eventually_hasSum_sub, opNNNorm_le_iff, ofSubsingleton_apply_apply, continuousMultilinearCurryRightEquiv_symm_apply', iteratedFDerivWithin_two_apply, bound, VectorFourier.fourierPowSMulRight_apply, NormedSpace.expSeries_eq_expSeries_rat, ContinuousAlternatingMap.coe_toContinuousMultilinearMap, map_sum_finset, uncurry0_apply, le_of_opNorm_le, FormalMultilinearSeries.comp_rightInv, curryLeft_apply, OrderedFinpartition.applyOrderedFinpartition_update_left, DifferentiableWithinAt.continuousMultilinear_apply_const, analyticWithinAt, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, toUniformOnFun_toFun, coe_restrictScalars, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, VectorFourier.fourierIntegral_continuousMultilinearMap_apply, HasFPowerSeriesOnBall.image_sub_sub_deriv_le, smulRight_apply, iteratedFDerivWithin_clm_apply_const_apply, currySum_apply, continuousMultilinearCurryRightEquiv_apply', compAlongComposition_apply, ContDiffWithinAt.iteratedFDerivWithin_comp_perm, Real.fourier_continuousMultilinearMap_apply, norm_map_insertNth_le, HasFPowerSeriesAt.coeff_zero, HasFPowerSeriesOnBall.hasSum_sub, iteratedFDeriv_two_apply, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition, continuousMultilinearCurryLeftEquiv_symm_apply, zero_apply, FormalMultilinearSeries.applyComposition_update, ext_iff, iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, continuousMultilinearCurryFin1_symm_apply, Quaternion.hasSum_expSeries_of_imaginary, opNorm_le_iff, iteratedDeriv_vcomp_two, map_zero, norm_map_cons_le, continuousMapClass, FormalMultilinearSeries.derivSeries_apply_diag, iteratedFDeriv_clm_apply_const_apply, HasFPowerSeriesWithinOnBall.hasSum, fderivCompContinuousLinearMap_apply, curryFinFinset_symm_apply, FormalMultilinearSeries.id_apply_one, apply_zero_uncurry0, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod, FormalMultilinearSeries.summable, FormalMultilinearSeries.compContinuousLinearMap_apply, FormalMultilinearSeries.summable_norm_apply, FormalMultilinearSeries.compAlongOrderedFinpartition_apply, le_opNorm_mul_pow_of_le, le_opNNNorm, FormalMultilinearSeries.comp_rightInv_aux2, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, continuousMultilinearCurryRightEquiv_apply, analyticOnNhd_uncurry_of_linear, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, HasStrictFDerivAt.continuousMultilinearMap_apply, curryFinFinset_apply, OrderedFinpartition.applyOrderedFinpartition_update_right, ContinuousLinearMap.norm_map_removeNth_le, hasStrictFDerivAt_uncurry, Real.fourierIntegral_continuousMultilinearMap_apply', compContinuousLinearMapContinuousMultilinear_apply_apply, norm_image_sub_le', iteratedFDerivWithin_zero_apply, NormedSpace.expSeries_hasSum_exp_of_mem_ball, prod_apply, FormalMultilinearSeries.applyComposition_ones, fin0_apply_norm, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum, TrivSqZeroExt.snd_expSeries_of_smul_comm, IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, PiTensorProduct.mapLMultilinear_toFun_apply, iteratedDerivWithin_vcomp_three, iteratedFDeriv_succ_apply_left, HasFDerivAt.continuousMultilinearMap_apply, continuousMultilinearCurryFin1_apply
instAdd 📖	CompOp	11 math math: toMultilinearMap_add, iteratedFDeriv_add_apply, iteratedFDeriv_add, iteratedFDerivWithin_add_apply, opNorm_add_le, add_apply, FormalMultilinearSeries.add_apply, ContinuousAlternatingMap.toContinuousMultilinearMap_add, add_prod_add, iteratedFDerivWithin_add_apply', iteratedFDeriv_add_apply'
instAddCommGroup 📖	CompOp	42 math math: fderiv_iteratedFDeriv, ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasFTaylorSeriesUpToOn_top_iff_right, iteratedFDerivWithin_succ_eq_comp_left, contDiffOn_iff_continuousOn_differentiableOn, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, norm_smulRightL_le, VectorFourier.fourierPowSMulRight_eq_comp, contDiffOn_nat_iff_continuousOn_differentiableOn, ContDiff.differentiable_iteratedFDeriv, instIsUniformAddGroup, hasFTaylorSeriesUpToOn_top_iff', contDiff_iff_continuous_differentiable, hasFTaylorSeriesUpToOn_succ_iff_right, ContinuousLinearMap.coe_flipMultilinearEquiv, hasFTaylorSeriesUpTo_top_iff', fderivWithin_iteratedFDerivWithin, hasFTaylorSeriesUpTo_succ_nat_iff_right, hasFTaylorSeriesUpToOn_succ_nat_iff_right, PiTensorProduct.dualSeminorms_bounded, iteratedFDerivWithin_succ_apply_left, HasFTaylorSeriesUpToOn.fderivWithin, PiTensorProduct.injectiveSeminorm_apply, norm_fderiv_iteratedFDeriv, norm_fderivWithin_iteratedFDerivWithin, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, contDiff_nat_iff_continuous_differentiable, hasStrictFDerivAt_compContinuousLinearMap, hasFTaylorSeriesUpToOn_succ_iff_left, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, smulRightL_apply, iteratedFDeriv_succ_eq_comp_left, ContDiffAt.differentiableAt_iteratedFDeriv, HasFTaylorSeriesUpTo.fderiv, ContDiffOn.differentiableOn_iteratedFDerivWithin, instIsTopologicalAddGroup, hasStrictFDerivAt_uncurry, compContinuousLinearMapContinuousMultilinear_apply_apply, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, iteratedFDeriv_succ_apply_left
instDistribMulAction 📖	CompOp	—
instInhabited 📖	CompOp	—
instModule 📖	CompOp	199 math math: fderiv_iteratedFDeriv, FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite, norm_iteratedFDerivComponent_le, ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasFTaylorSeriesUpToOn_top_iff_right, ContDiffMapSupportedIn.iteratedFDerivLM_apply, ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, FormalMultilinearSeries.changeOriginSeriesTerm_apply, changeOrigin_toFormalMultilinearSeries, ContDiffMapSupportedIn.structureMapCLM_apply, iteratedFDerivWithin_succ_eq_comp_right, HasFTaylorSeriesUpTo.hasFDerivAt, MultilinearMap.mkContinuousMultilinear_apply, norm_compContinuousLinearMapLRight_le, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, piLinearEquiv_symm_apply, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, HasFDerivWithinAt.linear_multilinear_comp, iteratedFDerivWithin_succ_eq_comp_left, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_gt, contDiffOn_iff_continuousOn_differentiableOn, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, HasFTaylorSeriesUpToOn.zero_eq', norm_smulRightL_le, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_eq_of_scalars, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, VectorFourier.fourierPowSMulRight_eq_comp, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, ContinuousLinearMap.flipMultilinear_apply_apply, uncurrySum_apply, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, curryFinFinset_symm_apply_const, HasFPowerSeriesOnBall.fderiv_eq, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, curryLeft_norm, isBoundedBilinearMap_compMultilinear, ContDiffMapSupportedIn.structureMapLM_eq_of_scalars, HasFPowerSeriesWithinAt.fderivWithin_eq, restrictScalarsLinear_apply, contDiffOn_nat_iff_continuousOn_differentiableOn, ContDiff.differentiable_iteratedFDeriv, ContDiffMapSupportedIn.uniformSpace_eq_iInf, PiTensorProduct.liftIsometry_tprodL, ContDiffMapSupportedIn.continuous_iff_comp_withOrder, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, FormalMultilinearSeries.iteratedFDerivSeries_eq_zero, iteratedFDerivWithin_eq_equiv_comp, ContDiffMapSupportedIn.structureMapCLM_zero_apply, ofSubsingletonₗᵢ_symm_apply, continuousMultilinearCurryFin0_symm_apply, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, continuousMultilinearCurryRightEquiv_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, hasFTaylorSeriesUpToOn_top_iff', ContinuousAlternatingMap.toContinuousMultilinearMapLI_apply, ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear, OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply, contDiff_iff_continuous_differentiable, prodL_apply, hasFTaylorSeriesUpToOn_succ_iff_right, ContinuousLinearMap.coe_flipMultilinearEquiv, PiTensorProduct.liftEquiv_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, PiTensorProduct.liftEquiv_apply, hasFTaylorSeriesUpTo_top_iff', fderivWithin_iteratedFDerivWithin, MultilinearMap.mkContinuousLinear_norm_le, piLinearEquiv_apply, ContinuousLinearMap.uncurryLeft_apply, curryFinFinset_apply_const, compContinuousLinearMapLRight_apply, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, apply_apply, flipLinear_apply_apply, hasFTaylorSeriesUpTo_succ_nat_iff_right, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, iteratedFDeriv_eq_equiv_comp, hasFTaylorSeriesUpToOn_succ_nat_iff_right, ContinuousAlternatingMap.toContinuousMultilinearMapLinear_apply, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, HasFPowerSeriesAt.fderiv_eq, continuousMultilinearCurryFin0_apply, PiTensorProduct.dualSeminorms_bounded, curryMidEquiv_apply, iteratedFDerivWithin_succ_apply_left, HasFTaylorSeriesUpToOn.fderivWithin, ContinuousLinearMap.norm_map_tail_le, PiTensorProduct.injectiveSeminorm_apply, norm_fderiv_iteratedFDeriv, HasFTaylorSeriesUpToOn.hasFDerivAt, iteratedDeriv_eq_equiv_comp, MultilinearMap.mkContinuousLinear_norm_le', norm_fderivWithin_iteratedFDerivWithin, HasFTaylorSeriesUpToOn.shift_of_succ, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, ContinuousLinearMap.continuous_uncurry_of_multilinear, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, MultilinearMap.mkContinuousMultilinear_norm_le', curryFinFinset_symm_apply_piecewise_const, ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft, FormalMultilinearSeries.leftInv_coeff_one, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, HasFPowerSeriesAt.hasFDerivAt, ContinuousLinearMap.uncurryMid_apply, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, PiTensorProduct.liftIsometry_comp_mapL, continuousMultilinearCurryLeftEquiv_apply, PiTensorProduct.liftIsometry_symm_apply, iteratedFDerivComponent_apply, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, iteratedFDeriv_succ_eq_comp_right, changeOriginSeries_support, ContDiffMapSupportedIn.seminorm_apply, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, HasFPowerSeriesWithinOnBall.fderivWithin_eq, piₗᵢ_symm_apply, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, contDiff_nat_iff_continuous_differentiable, MultilinearMap.mkContinuousMultilinear_norm_le, hasStrictFDerivAt_compContinuousLinearMap, HasFPowerSeriesOnBall.hasFDerivAt, curryMid_apply, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, HasFDerivAt.linear_multilinear_comp, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply, compContinuousLinearMapL_apply, PiTensorProduct.liftIsometry_apply_apply, prodL_symm_apply, iteratedFDeriv_zero_eq_comp, hasFTaylorSeriesUpToOn_succ_iff_left, continuousMultilinearCurryRightEquiv_symm_apply', ContDiffMapSupportedIn.structureMapLM_zero_injective, iteratedDerivWithin_eq_equiv_comp, curryLeft_apply, iteratedFDerivWithin_zero_eq_comp, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, currySum_apply, continuousMultilinearCurryRightEquiv_apply', HasFiniteFPowerSeriesOnBall.hasFDerivAt, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply, FormalMultilinearSeries.changeOriginSeries_finite_of_finite, ContDiffMapSupportedIn.continuous_iff_comp, continuousMultilinearCurryLeftEquiv_symm_apply, smulRightL_apply, iteratedFDeriv_succ_eq_comp_left, ContDiffMapSupportedIn.structureMapCLM_zero_injective, piₗᵢ_apply, ofSubsingletonₗᵢ_apply, continuousMultilinearCurryFin1_symm_apply, ContDiffAt.differentiableAt_iteratedFDeriv, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm, FormalMultilinearSeries.norm_changeOriginSeriesTerm, fderivCompContinuousLinearMap_apply, HasFTaylorSeriesUpTo.zero_eq', curryFinFinset_symm_apply, HasFTaylorSeriesUpTo.fderiv, HasFiniteFPowerSeriesOnBall.fderiv_eq, HasFPowerSeriesAt.hasStrictFDerivAt, isBoundedLinearMap_continuousMultilinearMap_comp_linear, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm, ContDiffMapSupportedIn.iteratedFDerivLM_eq_of_scalars, ContDiffOn.differentiableOn_iteratedFDerivWithin, norm_compContinuousLinearMapL_le, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, continuousMultilinearCurryRightEquiv_apply, ContDiffMapSupportedIn.structureMapLM_zero_apply, HasFPowerSeriesWithinAt.hasFDerivWithinAt, FormalMultilinearSeries.rightInv_coeff_one, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, ContinuousLinearMap.fpowerSeries_apply_one, toMultilinearMapLinear_apply, curryFinFinset_apply, FormalMultilinearSeries.changeOriginSeriesTerm_bound, ContinuousLinearMap.norm_map_removeNth_le, hasStrictFDerivAt_uncurry, compContinuousLinearMapContinuousMultilinear_apply_apply, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, ContDiffMapSupportedIn.structureMapLM_apply, isBoundedLinearMap_prod_multilinear, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, norm_curryMid, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_le, curryMidEquiv_symm_apply, iteratedFDeriv_succ_apply_left, continuousMultilinearCurryFin1_apply
instMulAction 📖	CompOp	—
instNeg 📖	CompOp	7 math math: iteratedFDerivWithin_neg_apply, neg_apply, iteratedFDeriv_neg_apply, FormalMultilinearSeries.neg_apply, neg_prod_neg, FormalMultilinearSeries.rightInv_coeff, iteratedFDeriv_neg
instSMul 📖	CompOp	18 math math: FormalMultilinearSeries.smul_apply, VectorFourier.fourierPowSMulRight_eq_comp, opNorm_smul_le, iteratedFDerivWithin_const_smul_apply, iteratedFDeriv_const_smul_apply, iteratedFDeriv_const_smul_apply', smul_prod_smul, instContinuousConstSMul, instIsBoundedSMul, instIsScalarTower, smul_apply, alternatization_apply_toContinuousMultilinearMap, instUniformContinuousConstSMul, instContinuousSMul, instSMulCommClass, instIsCentralScalar, ContinuousAlternatingMap.toContinuousMultilinearMap_smul, toMultilinearMap_smul
instSub 📖	CompOp	6 math math: ContDiffPointwiseHolderAt.isBigO, contDiffPointwiseHolderAt_iff, sub_apply, FormalMultilinearSeries.sub_apply, OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, sub_prod_sub
instZero 📖	CompOp	42 math math: FormalMultilinearSeries.removeZero_coeff_zero, FormalMultilinearSeries.ofScalars_eq_zero_of_scalar_zero, opNorm_zero_iff, HasFiniteFPowerSeriesAt.finite, iteratedFDerivWithin_succ_const, FormalMultilinearSeries.ofScalars_eq_zero, iteratedFDeriv_succ_const, FormalMultilinearSeries.coeff_eq_zero, hasBasis_nhds_zero, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three, ContinuousAlternatingMap.toContinuousMultilinearMap_zero, ContinuousLinearMap.fpowerSeries_apply_add_two, opNorm_zero, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, instIsBoundedSMul, constFormalMultilinearSeries_apply_of_nonzero, toMultilinearMap_zero, ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl, mkPiRing_zero, support_iteratedFDeriv_subset, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, HasCompactSupport.iteratedFDeriv, changeOriginSeries_support, tsupport_iteratedFDeriv_subset, FormalMultilinearSeries.apply_eq_zero_of_lt_order, hasBasis_nhds_zero_of_basis, iteratedFDeriv_zero_fun, ordinaryHypergeometricSeries_eq_zero_iff, HasFiniteFPowerSeriesOnBall.finite, FormalMultilinearSeries.id_apply_of_one_lt, FormalMultilinearSeries.order_eq_find, iteratedFDerivWithin_const_of_ne, iteratedFDerivWithin_zero_fun, zero_apply, mkPiRing_eq_zero_iff, ordinaryHypergeometricSeries_eq_zero_of_neg_nat, FormalMultilinearSeries.zero_apply, zero_prod_zero, FormalMultilinearSeries.comp_rightInv_aux2, constFormalMultilinearSeries_apply_succ, iteratedFDeriv_const_of_ne
linearDeriv 📖	CompOp	8 math math: changeOrigin_toFormalMultilinearSeries, linearDeriv_apply, ContinuousAlternatingMap.hasStrictFDerivAt, hasStrictFDerivAt, hasFDerivAt, ContinuousAlternatingMap.hasFDerivWithinAt, ContinuousAlternatingMap.hasFDerivAt, hasStrictFDerivAt_uncurry
mkPiAlgebra 📖	CompOp	6 math math: mkPiAlgebra_apply, norm_mkPiAlgebra_le, VectorFourier.fourierPowSMulRight_eq_comp, mkPiAlgebra_eq_mkPiAlgebraFin, norm_mkPiAlgebra, norm_mkPiAlgebra_of_empty
mkPiAlgebraFin 📖	CompOp	8 math math: mkPiAlgebraFin_apply, norm_mkPiAlgebraFin_zero, norm_mkPiAlgebraFin_le_of_pos, mkPiAlgebra_eq_mkPiAlgebraFin, norm_mkPiAlgebraFin_le, norm_mkPiAlgebraFin_succ_le, FormalMultilinearSeries.ofScalars_norm_eq_mul, norm_mkPiAlgebraFin
mkPiRing 📖	CompOp	8 math math: norm_mkPiRing, mkPiRing_apply_one_eq_self, mkPiRing_apply, spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul, FormalMultilinearSeries.mkPiRing_coeff_eq, mkPiRing_zero, mkPiRing_eq_iff, mkPiRing_eq_zero_iff
ofSubsingleton 📖	CompOp	12 math math: ContinuousAlternatingMap.ofSubsingleton_apply_toContinuousMultilinearMap, ofSubsingleton_symm_apply_apply, ofSubsingletonₗᵢ_symm_apply, norm_ofSubsingleton_id_le, nnnorm_ofSubsingleton, ofSubsingleton_apply_toMultilinearMap, ofSubsingleton_apply_apply, nnnorm_ofSubsingleton_id_le, nnnorm_ofSubsingleton_id, norm_ofSubsingleton, ofSubsingletonₗᵢ_apply, norm_ofSubsingleton_id
pi 📖	CompOp	8 math math: piLinearEquiv_apply, pi_apply, opNorm_pi, piEquiv_apply, opNNNorm_pi, coe_pi, piₗᵢ_apply, hasFTaylorSeriesUpToOn_pi
piEquiv 📖	CompOp	2 math math: piEquiv_apply, piEquiv_symm_apply
piLinearEquiv 📖	CompOp	2 math math: piLinearEquiv_symm_apply, piLinearEquiv_apply
prod 📖	CompOp	14 math math: eq_prod_iff, smul_prod_smul, iteratedFDerivWithin_prodMk, prodEquiv_apply, opNNNorm_prod, HasFTaylorSeriesUpToOn.prodMk, iteratedFDeriv_prodMk, neg_prod_neg, sub_prod_sub, zero_prod_zero, opNorm_prod, isBoundedLinearMap_prod_multilinear, prod_apply, add_prod_add
prodEquiv 📖	CompOp	6 math math: prodEquiv_symm_apply_fst, prodL_apply, prodEquiv_symm_apply, prodEquiv_apply, prodEquiv_symm_apply_snd, prodL_symm_apply
restrictScalars 📖	CompOp	11 math math: isEmbedding_restrictScalars, restrictScalarsLinear_apply, ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq, uniformContinuous_restrictScalars, norm_restrictScalars, ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq, ContDiffAt.restrictScalars_iteratedFDeriv, coe_restrictScalars, fderivWithin_restrictScalars_comp, isUniformEmbedding_restrictScalars, continuous_restrictScalars
smulRight 📖	CompOp	6 math math: ContinuousAlternatingMap.smulRight_toContinuousMultilinearMap, smulRight_toMultilinearMap, smulRight_apply, smulRightL_apply, nnnorm_smulRight, norm_smulRight
toContinuousLinearMap 📖	CompOp	9 math math: HasFDerivWithinAt.continuousMultilinearMap_apply, HasFDerivWithinAt.linear_multilinear_comp, HasFDerivAt.multilinear_comp, toContinuousLinearMap_apply, HasFDerivWithinAt.multilinear_comp, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMap_apply, HasFDerivAt.continuousMultilinearMap_apply
toMultilinearMap 📖	CompOp	22 math math: coe_coe, toMultilinearMap_add, domDomCongr_toMultilinearMap, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, constOfIsEmpty_toMultilinearMap, PiTensorProduct.norm_eval_le_injectiveSeminorm, PiTensorProduct.liftEquiv_apply, ContinuousAlternatingMap.map_eq_zero_of_eq', toMultilinearMap_zero, cont, PiTensorProduct.mapLMultilinear_apply_apply, toMultilinearMap_injective, codRestrict_toMultilinearMap, ofSubsingleton_apply_toMultilinearMap, PiTensorProduct.liftIsometry_apply_apply, alternatization_apply_toAlternatingMap, PiTensorProduct.norm_eval_le_projectiveSeminorm, smulRight_toMultilinearMap, toMultilinearMap_smul, toMultilinearMapLinear_apply, PiTensorProduct.mapLMultilinear_toFun_apply, PiTensorProduct.tprodL_coe
toMultilinearMapLinear 📖	CompOp	1 math math: toMultilinearMapLinear_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
add_prod_add 📖	mathematical	—	prod ContinuousMultilinearMap instAdd Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd Prod.continuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid	—	—
codRestrict_apply_coe 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousMultilinearMap funLike	Submodule.addCommMonoid Submodule.module instTopologicalSpaceSubtype codRestrict	—	—
codRestrict_toMultilinearMap 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousMultilinearMap funLike	toMultilinearMap Submodule.addCommMonoid Submodule.module instTopologicalSpaceSubtype codRestrict MultilinearMap.codRestrict	—	—
coe_coe 📖	mathematical	—	DFunLike.coe MultilinearMap MultilinearMap.instFunLikeForall toMultilinearMap ContinuousMultilinearMap funLike	—	—
coe_continuous 📖	mathematical	—	Continuous Pi.topologicalSpace DFunLike.coe ContinuousMultilinearMap funLike	—	cont
coe_pi 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap Pi.addCommMonoid Pi.module Pi.topologicalSpace funLike pi	—	—
coe_restrictScalars 📖	mathematical	IsScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe ContinuousMultilinearMap funLike restrictScalars	—	—
compContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike compContinuousLinearMap ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	—
cons_add 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Fin.cons AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.cons_add
cons_smul 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Fin.cons SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.cons_smul
constOfIsEmpty_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike constOfIsEmpty	—	—
constOfIsEmpty_toMultilinearMap 📖	mathematical	—	toMultilinearMap constOfIsEmpty MultilinearMap.constOfIsEmpty	—	—
cont 📖	mathematical	—	Continuous Pi.topologicalSpace MultilinearMap.toFun toMultilinearMap	—	—
continuousMapClass 📖	mathematical	—	ContinuousMapClass ContinuousMultilinearMap Pi.topologicalSpace funLike	—	cont
domDomCongrEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMultilinearMap EquivLike.toFunLike Equiv.instEquivLike domDomCongrEquiv domDomCongr	—	—
domDomCongrEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMultilinearMap EquivLike.toFunLike Equiv.instEquivLike Equiv.symm domDomCongrEquiv domDomCongr	—	—
domDomCongr_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike domDomCongr Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
domDomCongr_toMultilinearMap 📖	mathematical	—	toMultilinearMap domDomCongr MultilinearMap.domDomCongr	—	—
eq_prod_iff 📖	mathematical	—	prod ContinuousLinearMap.compContinuousMultilinearMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd ContinuousLinearMap.fst ContinuousLinearMap.snd	—	prod_ext_iff
ext 📖	—	DFunLike.coe ContinuousMultilinearMap funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike	—	ext
ext_ring 📖	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	toMultilinearMap_injective MultilinearMap.ext_ring
ext_ring_iff 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext_ring
instIsCentralScalar 📖	mathematical	—	IsCentralScalar ContinuousMultilinearMap instSMul MulOpposite ContinuousConstSMul.op SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass SMulCommClass.op_right DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ContinuousConstSMul.op SMulCommClass.op_right ext IsCentralScalar.op_smul_eq_smul
instIsScalarTower 📖	mathematical	—	IsScalarTower ContinuousMultilinearMap instSMul	—	ext smul_assoc
instSMulCommClass 📖	mathematical	—	SMulCommClass ContinuousMultilinearMap instSMul	—	ext SMulCommClass.smul_comm
linearDeriv_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Pi.topologicalSpace Pi.addCommMonoid Pi.module ContinuousLinearMap.funLike linearDeriv Finset.sum Finset.univ ContinuousMultilinearMap funLike Function.update	—	Finset.sum_congr ContinuousLinearMap.coe_sum' Finset.sum_apply
map_add_univ 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.sum Finset Finset.univ Finset.fintype Finset.piecewise Finset.decidableMem	—	MultilinearMap.map_add_univ
map_coord_zero 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe ContinuousMultilinearMap funLike	—	MultilinearMap.map_coord_zero
map_piecewise_add 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Finset.piecewise Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.decidableMem Finset.sum Finset Finset.powerset	—	MultilinearMap.map_piecewise_add
map_piecewise_smul 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring funLike Finset.piecewise SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.decidableMem Finset.prod CommSemiring.toCommMonoid	—	MultilinearMap.map_piecewise_smul
map_smul_univ 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring funLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommSemiring.toCommMonoid Finset.univ	—	MultilinearMap.map_smul_univ
map_sum 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Finset.sum Finset.univ Pi.instFintype	—	MultilinearMap.map_sum
map_sum_finset 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Finset.sum Fintype.piFinset	—	MultilinearMap.map_sum_finset
map_update_add 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Function.update AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.map_update_add'
map_update_smul 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Function.update SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.map_update_smul'
map_update_sub 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike Function.update SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	MultilinearMap.map_update_sub
map_zero 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	MultilinearMap.map_zero
mkPiAlgebraFin_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule funLike mkPiAlgebraFin Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
mkPiAlgebra_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule funLike mkPiAlgebra Finset.prod CommSemiring.toCommMonoid Finset.univ	—	—
mkPiAlgebra_eq_mkPiAlgebraFin 📖	mathematical	—	mkPiAlgebra Fin.fintype mkPiAlgebraFin CommSemiring.toSemiring	—	ext List.prod_ofFn
mkPiRing_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule funLike mkPiRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommRing.toCommMonoid Finset.univ	—	—
mkPiRing_apply_one_eq_self 📖	mathematical	—	mkPiRing DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule funLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	toMultilinearMap_injective MultilinearMap.mkPiRing_apply_one_eq_self
mkPiRing_eq_iff 📖	mathematical	—	mkPiRing	—	toMultilinearMap_injective MultilinearMap.mkPiRing_eq_iff
mkPiRing_eq_zero_iff 📖	mathematical	—	mkPiRing ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	mkPiRing_zero mkPiRing_eq_iff
mkPiRing_zero 📖	mathematical	—	mkPiRing AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instZero	—	ext_ring Finite.of_fintype mkPiRing_apply smul_zero zero_apply
neg_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
neg_prod_neg 📖	mathematical	—	prod Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap instNeg Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd Prod.instAddCommGroup Prod.instIsTopologicalAddGroup AddCommGroup.toAddGroup	—	—
ofSubsingleton_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.funLike	—	—
ofSubsingleton_apply_toMultilinearMap 📖	mathematical	—	toMultilinearMap DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton LinearMap MultilinearMap MultilinearMap.ofSubsingleton ContinuousLinearMap.toLinearMap	—	—
ofSubsingleton_symm_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike Equiv ContinuousMultilinearMap EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofSubsingleton funLike	—	—
piEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMultilinearMap Pi.addCommMonoid Pi.module Pi.topologicalSpace EquivLike.toFunLike Equiv.instEquivLike piEquiv pi	—	—
piEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMultilinearMap Pi.addCommMonoid Pi.module Pi.topologicalSpace EquivLike.toFunLike Equiv.instEquivLike Equiv.symm piEquiv ContinuousLinearMap.compContinuousMultilinearMap ContinuousLinearMap.proj	—	—
piLinearEquiv_apply 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousConstSMul	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap Pi.addCommMonoid Pi.module Pi.topologicalSpace addCommMonoid Pi.continuousAdd AddSemigroup.toAdd instModule instContinuousConstSMulForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Pi.smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike piLinearEquiv pi	—	RingHomInvPair.ids Pi.continuousAdd instContinuousConstSMulForall Pi.smulCommClass
piLinearEquiv_symm_apply 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousConstSMul	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap Pi.addCommMonoid Pi.module Pi.topologicalSpace addCommMonoid Pi.continuousAdd AddSemigroup.toAdd instModule instContinuousConstSMulForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Pi.smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm piLinearEquiv ContinuousLinearMap.compContinuousMultilinearMap ContinuousLinearMap.proj	—	RingHomInvPair.ids Pi.continuousAdd instContinuousConstSMulForall Pi.smulCommClass
pi_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap Pi.addCommMonoid Pi.module Pi.topologicalSpace funLike pi	—	—
prodEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMultilinearMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd EquivLike.toFunLike Equiv.instEquivLike prodEquiv prod	—	—
prodEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousMultilinearMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd EquivLike.toFunLike Equiv.instEquivLike Equiv.symm prodEquiv ContinuousLinearMap.compContinuousMultilinearMap ContinuousLinearMap.fst ContinuousLinearMap.snd	—	—
prodEquiv_symm_apply_fst 📖	mathematical	—	ContinuousMultilinearMap DFunLike.coe Equiv Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd EquivLike.toFunLike Equiv.instEquivLike Equiv.symm prodEquiv ContinuousLinearMap.compContinuousMultilinearMap ContinuousLinearMap.fst	—	—
prodEquiv_symm_apply_snd 📖	mathematical	—	ContinuousMultilinearMap DFunLike.coe Equiv Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd EquivLike.toFunLike Equiv.instEquivLike Equiv.symm prodEquiv ContinuousLinearMap.compContinuousMultilinearMap ContinuousLinearMap.snd	—	—
prod_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd funLike prod	—	—
prod_ext 📖	—	ContinuousLinearMap.compContinuousMultilinearMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd ContinuousLinearMap.fst ContinuousLinearMap.snd	—	—	prod_ext_iff
prod_ext_iff 📖	mathematical	—	ContinuousLinearMap.compContinuousMultilinearMap Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd ContinuousLinearMap.fst ContinuousLinearMap.snd	—	prodEquiv_symm_apply Equiv.apply_eq_iff_eq
smulRight_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring 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 Semiring.toNonAssocSemiring Semiring.toModule	—	—
smulRight_toMultilinearMap 📖	mathematical	—	toMultilinearMap CommSemiring.toSemiring smulRight MultilinearMap.smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
smul_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass	—	—
smul_prod_smul 📖	mathematical	—	prod ContinuousMultilinearMap instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd Prod.distribSMul AddMonoid.toAddZeroClass Prod.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass Prod.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction Module.toDistribMulAction	—	—
sub_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid funLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
sub_prod_sub 📖	mathematical	—	prod Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap instSub Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd Prod.instAddCommGroup Prod.instIsTopologicalAddGroup AddCommGroup.toAddGroup	—	—
sum_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike Finset.sum addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
toContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike toContinuousLinearMap ContinuousMultilinearMap funLike Function.update	—	—
toMultilinearMapLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap MultilinearMap addCommMonoid MultilinearMap.addCommMonoid instModule MultilinearMap.instModule LinearMap.instFunLike toMultilinearMapLinear toMultilinearMap	—	—
toMultilinearMap_add 📖	mathematical	—	toMultilinearMap ContinuousMultilinearMap instAdd MultilinearMap MultilinearMap.instAdd	—	—
toMultilinearMap_injective 📖	mathematical	—	ContinuousMultilinearMap MultilinearMap toMultilinearMap	—	—
toMultilinearMap_smul 📖	mathematical	—	toMultilinearMap ContinuousMultilinearMap instSMul MultilinearMap MultilinearMap.instSMul	—	—
toMultilinearMap_zero 📖	mathematical	—	toMultilinearMap ContinuousMultilinearMap instZero MultilinearMap MultilinearMap.instZero	—	—
zero_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap funLike instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
zero_prod_zero 📖	mathematical	—	prod ContinuousMultilinearMap instZero Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd	—	—

ContinuousMultilinearMap.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
«term_[×_]→L[_]_» 📖	CompOp	—

---

← Back to Index