EuclideanSpace 📖 | CompOp | 189 mathmath: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, Pi.comul_eq_adjoint, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, EuclideanSpace.orthonormal_single, EuclideanSpace.closedBall_zero_eq, OrthonormalBasis.repr_injective, Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, Matrix.l2_opNorm_mulVec, EuclideanSpace.inner_single_left, EuclideanSpace.basisFun_toBasis, DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots, EuclideanSpace.norm_sq_eq, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, contMDiff_neg_sphere, SmoothBumpCovering.exists_immersion_euclidean, EuclideanHalfSpace.ext_iff, EuclideanSpace.basisFun_apply, Diffeology.isPlot_id', Matrix.IsHermitian.eigenvalues_eq, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, OrthonormalBasis.repr_self, Icc_isBoundaryPoint_bot, EuclideanSpace.nndist_eq, stereographic'_source, OrthonormalBasis.measurePreserving_repr, Matrix.IsHermitian.eigenvectorUnitary_col_eq, Matrix.toEuclideanLin_apply, mfderivWithin_projIcc_one, EuclideanSpace.norm_single, Euclidean.closedBall_eq_image, Quaternion.linearIsometryEquivTuple_symm_apply, Pi.counit_eq_adjoint, ProbabilityTheory.covarianceBilin_apply_basisFun_self, Icc_isInteriorPoint_interior, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, mfderivWithin_comp_projIcc_one, contDiffWithinAt_euclidean, EuclideanSpace.volume_closedBall_fin_three, IccLeftChart_extend_interior_pos, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Matrix.IsHermitian.eigenvectorUnitary_mulVec, EuclideanSpace.dist_single_same, Module.Basis.coe_toOrthonormalBasis_repr, contMDiff_coe_sphere, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, OrthonormalBasis.coe_ofRepr, EuclideanSpace.nnnorm_single, Complex.orthonormalBasisOneI_repr_apply, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, Matrix.toEuclideanCLM_toLp, Diffeology.IsPlot.dSmooth, EuclideanSpace.volume_closedBall_fin_two, Matrix.piLp_ofLp_toEuclideanLin, stereographic'_target, OrthonormalBasis.tensorProduct_repr_tmul_apply', Matrix.l2_opNNNorm_mulVec, frontier_range_modelWithCornersEuclideanHalfSpace, EuclideanSpace.instIsManifoldSphere, OrthonormalBasis.equiv_apply, Module.Basis.coe_toOrthonormalBasis_repr_symm, contMDiff_subtype_coe_Icc, OrthonormalBasis.repr_apply_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, EuclideanSpace.edist_single_same, EuclideanHalfSpace.convex, EuclideanSpace.sphere_zero_eq, LinearMap.toMatrix_innerₛₗ_apply, contDiffAt_euclidean, finrank_euclideanSpace, mfderiv_coe_sphere_injective, contDiffOn_euclidean, InnerProductGeometry.norm_ofLp_crossProduct, Matrix.ofLp_toEuclideanCLM, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, EuclideanQuadrant.convex, range_euclideanHalfSpace, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, IccLeftChart_extend_bot, Matrix.l2_opNNNorm_def, EuclideanSpace.basisFun_repr, OrthonormalBasis.equiv_apply_euclideanSpace, Complex.orthonormalBasisOneI_repr_symm_apply, Manifold.riemannianEDist_def, modelWithCornersEuclideanHalfSpace_zero, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, EuclideanSpace.norm_eq, Matrix.IsHermitian.eigenvectorUnitary_apply, EuclideanSpace.inner_eq_star_dotProduct, OrthonormalBasis.sum_repr_symm, contMDiffWithinAt_comp_projIcc_iff, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, EuclideanSpace.volume_ball_fin_three, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, ProbabilityTheory.covarianceBilin_apply_basisFun, Diffeology.isPlot_iff_contDiff, OrthonormalBasis.measurePreserving_repr_symm, Diffeology.isPlot_iff_dSmooth, oneTangentSpaceIcc_def, EuclideanQuadrant.ext_iff, IccRightChart_extend_top_mem_frontier, hasFDerivWithinAt_euclidean, Matrix.IsHermitian.eigenvectorUnitary_coe, Matrix.toEuclideanLin_eq_toLin, Euclidean.closedBall_eq_preimage, Matrix.isHermitian_iff_isSymmetric, EuclideanSpace.basisFun_inner, InnerProductSpace.toMatrix_rankOne, differentiableAt_euclidean, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, range_euclideanQuadrant, mdifferentiableWithinAt_comp_projIcc_iff, Diffeology.isOpen_iff_preimages_plots, differentiableOn_euclidean, Diffeology.IsContDiffCompatible.isPlot_iff, EuclideanSpace.ball_zero_eq, range_mfderiv_coe_sphere, Diffeology.IsPlot.continuous, Matrix.ofLp_toEuclideanLin_apply, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.inner_basisFun_real, iccLeftChart_extend_zero, Euclidean.ball_eq_preimage, EuclideanSpace.volume_ball, OrthonormalBasis.repr_symm_single, interior_range_modelWithCornersEuclideanHalfSpace, toMatrix_innerSL_apply, Diffeology.IsPlot.contDiff, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', Matrix.toEuclideanLin_apply_piLp_toLp, EuclideanSpace.dist_eq, Diffeology.isPlot_id, contMDiffOn_comp_projIcc_iff, volume_euclideanSpace_eq_dirac, OrthonormalBasis.coe_toBasis_repr, OrthonormalBasis.sum_repr, EuclideanSpace.infinite, exists_embedding_euclidean_of_compact, OrthonormalBasis.coe_toBasis_repr_apply, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OrthonormalBasis.coe_equiv_euclideanSpace, EuclideanSpace.dist_sq_eq, Matrix.IsHermitian.eigenvectorUnitary_transpose_apply, stereographic'_symm_apply, EuclideanSpace.coe_measurableEquiv, NumberField.mixedEmbedding.euclidean.finrank, EuclideanSpace.nnnorm_eq, range_modelWithCornersEuclideanHalfSpace, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, EuclideanSpace.inner_single_right, Matrix.toEuclideanLin_eq_toLin_orthonormal, EuclideanSpace.measurableEquiv_toEquiv, Matrix.cstar_norm_def, ContMDiff.codRestrict_sphere, Quaternion.linearIsometryEquivTuple_apply, mfderiv_subtype_coe_Icc_one, Diffeology.IsPlot.dSmooth_comp, EuclideanSpace.single_eq_zero_iff, Matrix.IsHermitian.mulVec_eigenvectorBasis, Matrix.l2_opNorm_def, Matrix.toEuclideanLin_toLp, OrthonormalBasis.measurePreserving_measurableEquiv, EuclideanSpace.nndist_single_same, EuclideanSpace.edist_eq, Pi.orthonormalBasis_repr, IccRightChart_extend_top, boundary_Icc, DiffeologicalSpace.CorePlotsOn.isPlotOn_univ, EuclideanSpace.volume_closedBall, finrank_euclideanSpace_fin, boundary_product, OrthonormalBasis.repr_reindex, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, EuclideanSpace.coe_measurableEquiv_symm, contDiff_euclidean, IccLeftChart_extend_bot_mem_frontier, OrthonormalBasis.tensorProduct_repr_tmul_apply, Icc_isBoundaryPoint_top, instIsManifoldIcc, Diffeology.dSmooth_iff, contMDiffOn_projIcc, DiffeologicalSpace.isOpen_iff_preimages_plots, contMDiff_circleExp, hasStrictFDerivAt_euclidean
|