Basic

📁 Source: Mathlib/Analysis/InnerProductSpace/Basic.lean

Statistics

Metric	Count
Definitions rclikeToReal, complexToReal, rclikeToReal, innerProductSpace, toInnerProductSpaceReal, bilinFormOfRealInner, innerₗ, innerₛₗ, instInnerProductSpaceRealComplex, sesqFormOfInner	10
Theorems inner, inner_sum, sum_inner, inner_sum, sum_inner, inner_apply, inner_apply', abs_real_inner_div_norm_mul_norm_eq_one_iff, abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul, abs_real_inner_div_norm_mul_norm_le_one, abs_real_inner_le_norm, coe_innerₛₗ_apply, dist_div_norm_sq_smul, eq_of_norm_le_re_inner_eq_norm_sq, ext_iff_inner_left, ext_iff_inner_right, ext_inner_left, ext_inner_right, flip_innerₗ, im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four, inner_add_add_self, inner_add_left, inner_add_right, inner_conj_symm, inner_eq_neg_one_iff_of_norm_eq_one, inner_eq_norm_mul_iff, inner_eq_norm_mul_iff_div, inner_eq_norm_mul_iff_real, inner_eq_norm_sq_left_iff, inner_eq_norm_sq_right_iff, inner_eq_ofReal_norm_sq_left_iff, inner_eq_ofReal_norm_sq_right_iff, inner_eq_one_iff_of_norm_eq_one, inner_eq_one_iff_of_norm_one, inner_eq_sum_norm_sq_div_four, inner_eq_zero_of_left, inner_eq_zero_of_right, inner_eq_zero_symm, inner_im_symm, inner_lt_norm_mul_iff_real, inner_lt_one_iff_real_of_norm_eq_one, inner_lt_one_iff_real_of_norm_one, inner_mul_inner_self_le, inner_mul_symm_re_eq_norm, inner_neg_left, inner_neg_neg, inner_neg_right, inner_re_symm, inner_re_zero_left, inner_re_zero_right, inner_self_conj, inner_self_eq_norm_mul_norm, inner_self_eq_norm_sq, inner_self_eq_norm_sq_to_K, inner_self_eq_one_of_norm_eq_one, inner_self_eq_one_of_norm_one, inner_self_eq_zero, inner_self_im, inner_self_ne_zero, inner_self_nonneg, inner_self_ofReal_norm, inner_self_ofReal_re, inner_self_re_eq_norm, inner_smul_left, inner_smul_left_eq_smul, inner_smul_left_eq_star_smul, inner_smul_real_left, inner_smul_real_right, inner_smul_right, inner_smul_right_eq_smul, inner_sub_left, inner_sub_right, inner_sub_sub_self, inner_sum, inner_sum_smul_sum_smul_of_sum_eq_zero, inner_zero_left, inner_zero_right, innerₗ_apply_apply, innerₛₗ_apply_apply, instSymmEqInnerOfNat, isNonneg_inner, isPosSemidef_inner, isSymm_inner, linearIndependent_of_ne_zero_of_inner_eq_zero, neg_one_le_real_inner_of_norm_eq_one, nnnorm_inner_le_nnnorm, norm_add_eq_iff_real, norm_add_eq_sqrt_iff_real_inner_eq_zero, norm_add_mul_self, norm_add_mul_self_real, norm_add_pow_two, norm_add_pow_two_real, norm_add_sq, norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real, norm_add_sq_real, norm_eq_sqrt_re_inner, norm_eq_sqrt_real_inner, norm_inner_div_norm_mul_norm_eq_one_iff, norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul, norm_inner_eq_norm_iff, norm_inner_eq_norm_tfae, norm_inner_le_norm, norm_inner_symm, norm_sub_eq_norm_add, norm_sub_eq_sqrt_iff_real_inner_eq_zero, norm_sub_mul_self, norm_sub_mul_self_real, norm_sub_pow_two, norm_sub_pow_two_real, norm_sub_sq, norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, norm_sub_sq_eq_norm_sq_add_norm_sq_real, norm_sub_sq_real, parallelogram_law, parallelogram_law_with_nnnorm, parallelogram_law_with_nnnorm_mul, parallelogram_law_with_norm, parallelogram_law_with_norm_mul, re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four, re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, re_inner_le_norm, re_inner_self_nonpos, re_inner_self_pos, real_inner_I_smul_self, real_inner_add_add_self, real_inner_add_sub_eq_zero_iff, real_inner_comm, real_inner_div_norm_mul_norm_eq_neg_one_iff, real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul, real_inner_div_norm_mul_norm_eq_one_iff, real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul, real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, real_inner_eq_re_inner, real_inner_le_norm, real_inner_le_one_of_norm_eq_one, real_inner_mem_Icc_of_norm_eq_one, real_inner_mul_inner_self_le, real_inner_self_abs, real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_sq, real_inner_self_nonneg, real_inner_self_nonpos, real_inner_self_pos, real_inner_smul_left, real_inner_smul_right, real_inner_smul_self_left, real_inner_smul_self_right, real_inner_sub_sub_self, sum_inner	153
Total	163

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	—	Inner.inner Real Complex InnerProductSpace.toInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instInnerProductSpaceRealComplex re instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	—

DFinsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_sum 📖	mathematical	—	Inner.inner InnerProductSpace.toInner sum AddZero.toZero AddZeroClass.toAddZero AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	inner_sum Finset.sum_congr
sum_inner 📖	mathematical	—	Inner.inner InnerProductSpace.toInner sum AddZero.toZero AddZeroClass.toAddZero AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	sum_inner Finset.sum_congr

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_sum 📖	mathematical	—	Inner.inner InnerProductSpace.toInner sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	inner_sum Finset.sum_congr
sum_inner 📖	mathematical	—	Inner.inner InnerProductSpace.toInner sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	sum_inner Finset.sum_congr

Inner

Definitions

Name	Category	Theorems
rclikeToReal 📖	CompOp	2 math math: real_inner_eq_re_inner, real_inner_I_smul_self

InnerProductSpace

Definitions

Name	Category	Theorems
complexToReal 📖	CompOp	—
rclikeToReal 📖	CompOp	1 math math: LinearMap.IsSymmetric.restrictScalars

RCLike

Definitions

Name	Category	Theorems
innerProductSpace 📖	CompOp	544 math math: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, Pi.comul_eq_adjoint, TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, UpperHalfPlane.mdifferentiable_num, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, hasSum_mellin_pi_mul_sq', TensorProduct.enorm_lid, continuousOn_stereoToFun, Distribution.dsupport_delta, CuspFormClass.holo, InnerProductSpace.toLinearIsometry_toDual, MeasureTheory.charFun_eq_fourierIntegral', PeriodPair.hasFPowerSeriesAt_weierstrassPExcept, LinearMap.toLinearMap_tracePositiveLinearMap, hasFDerivAt_iff_hasGradientAt, Real.fourierCoeff_tsum_comp_add, UnitAddTorus.coe_mFourierBasis, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, ModularFormClass.hasFPowerSeries_cuspFunction, ModularFormClass.qExpansionFormalMultilinearSeries_radius, InnerProductSpace.rankOne_one_left_eq_innerSL, Real.tsum_eq_tsum_fourier, EuclideanSpace.orthonormal_single, PeriodPair.coeff_weierstrassPExceptSeries, Complex.meromorphic_digamma, OrthonormalBasis.repr_injective, has_pointwise_sum_fourier_series_of_summable, PeriodPair.iteratedDeriv_weierstrassPExcept_self, Complex.GammaIntegral_eq_mellin, norm_jacobiTheta₂_term_fderiv_ge, Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, Matrix.l2_opNorm_mulVec, AnalyticOn.cpow, ValueDistribution.characteristic_mul_top_le, one_add_cpow_hasFPowerSeriesAt_zero, inner_apply', UpperHalfPlane.analyticAt_smul, linearIndependent_of_ne_zero_of_wInner_one_eq_zero, AddChar.wInner_cWeight_self, innerSL_apply_apply, LinearMap.adjoint_innerₛₗ_apply, EuclideanSpace.inner_single_left, EuclideanSpace.basisFun_toBasis, ContinuousLinearMap.innerSL_apply_comp_of_isSymmetric, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, TemperedDistribution.fourierMultiplierCLM_smul, circleIntegral.integral_sub_inv_of_mem_ball, fourierCoeffOn.const_mul, mellin_div_const, TemperedDistribution.lineDerivOp_fourier_eq, Matrix.spectrum_toLpLin, ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian, InnerProductSpace.toDual_symm_apply, AnalyticOnNhd.circleAverage_log_norm, EuclideanSpace.basisFun_apply, fourierIntegral_gaussian_innerProductSpace', MeasureTheory.charFun_toDual_symm_eq_charFunDual, fourier_gaussian_pi', MeasureTheory.charFun_eq_fourierIntegral, Differentiable.fderiv_norm_rpow, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self, TensorProduct.toLinearEquiv_lidIsometry, OrthonormalBasis.toBasis_singleton, inner_gradientWithin_right, Matrix.IsHermitian.eigenvalues_eq, Distribution.IsVanishingOn.smulLeftCLM, AnalyticWithinAt.cpow, HasFDerivAt.norm_sq, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, OrthonormalBasis.repr_self, differentiableOn_iteratedDerivWithin_cotTerm, HasDerivAt.hasGradientAt, HarmonicAt.analyticAt_complex_partial, OrthonormalBasis.measurePreserving_repr, SchwartzMap.integral_fourierInv_smul_eq, PeriodPair.analyticAt_weierstrassPExcept, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, Matrix.IsHermitian.eigenvectorUnitary_col_eq, ContinuousLinearMap.toSesqForm_apply_coe, fourier_gaussian_innerProductSpace, Matrix.toEuclideanLin_apply, TemperedDistribution.smulLeftCLM_neg, Function.HasTemperateGrowth.toTemperedDistribution_apply, LSeries_iteratedDeriv, Complex.analyticOnNhd_univ_iff_differentiable, Pi.counit_eq_adjoint, ProbabilityTheory.covarianceBilin_apply_basisFun_self, Complex.taylorSeries_eq_on_ball', fourierCoeff_bernoulli_eq, LDL.lowerInv_orthogonal, AddChar.wInner_cWeight_eq_zero_iff_ne, TemperedDistribution.instLineDerivLeftSMulReal, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, TemperedDistribution.fourierInv_lineDerivOp_eq, UpperHalfPlane.mdifferentiable_inv_denom, contDiffWithinAt_euclidean, Real.fourier_iteratedFDeriv, InnerProductSpace.toDualMap_apply_apply, UnitAddTorus.mFourierCoeff_toLp, Matrix.IsHermitian.eigenvectorUnitary_mulVec, TemperedDistribution.instFourierAdd, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, coe_innerSL_apply, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, LSeries_analyticOnNhd, TemperedDistribution.instFourierSMul, TensorProduct.lidIsometry_apply, AnalyticOnNhd.cpow, Module.Basis.coe_toOrthonormalBasis_repr, orthonormal_fourier, UpperHalfPlane.contMDiff_coe, CuspForm.holo', Differentiable.hasFPowerSeriesOnBall, BoundedContinuousFunction.mem_charPoly, HasGradientWithinAt.differentiableWithinAt, TemperedDistribution.delta_apply, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, fourierIntegral_gaussian_pi, hasSum_mellin, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, hasGradientWithinAt_iff_hasFDerivWithinAt, Matrix.gram_eq_conjTranspose_mul, DifferentiableOn.contDiffOn, TemperedDistribution.instContinuousFourier, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, OrthonormalBasis.coe_ofRepr, AnalyticAt.clog, UpperHalfPlane.contMDiff_inv_denom, Complex.orthonormalBasisOneI_repr_apply, SchwartzMap.delta_apply, norm_cauchyPowerSeries_le, hasFDerivAt_norm_rpow, fourier_gaussian_innerProductSpace', Matrix.toEuclideanCLM_toLp, hasSum_fourier_series_L2, ProbabilityTheory.iteratedDeriv_complexMGF, contDiffOn_stereoToFun, HilbertBasis.hasSum_repr, ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero, HasFDerivWithinAt.hasGradientWithinAt, innerSL_inj, StrongDual.toLp_of_not_memLp, TensorProduct.inner_lid_lid, Matrix.piLp_ofLp_toEuclideanLin, InnerProductSpace.toDual_apply, OrthonormalBasis.tensorProduct_repr_tmul_apply', EuclideanSpace.coe_proj, Matrix.l2_opNNNorm_mulVec, ValueDistribution.characteristic_sub_characteristic_inv_at_zero, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, InnerProductSpace.toDualMap_apply, MellinConvergent.div_const, ProbabilityTheory.analyticAt_complexMGF, AnalyticOn.clog, HurwitzZeta.hurwitzEvenFEPair_zero_symm, circleIntegral.integral_sub_zpow_of_undef, Matrix.isSymmetric_toEuclideanLin_iff, PeriodPair.weierstrassPExcept_eq_tsum, Orthonormal.isHilbertSum, OrthonormalBasis.singleton_apply, OrthonormalBasis.equiv_apply, TemperedDistribution.fourierMultiplierCLM_apply, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, AnalyticOnNhd.clog, Module.Basis.coe_toOrthonormalBasis_repr_symm, InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjointAux_apply, ProperCone.innerDual_singleton, TemperedDistribution.fourierMultiplierCLM_const, PeriodPair.meromorphic_derivWeierstrassP, InnerProductSpace.rankOne_def, stereoToFun_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, OrthonormalBasis.repr_apply_apply, ClosedSubmodule.orthogonal_eq_inter, MeasureTheory.L2.inner_indicatorConstLp_one, SchwartzMap.toTemperedDistributionCLM_apply_apply, HasDerivAtFilter.hasGradientAtFilter, TemperedDistribution.smulLeftCLM_sub, Complex.one_add_cpow_hasFPowerSeriesAt_zero, UpperHalfPlane.contMDiff_num, UpperHalfPlane.mdifferentiable_denom, LinearMap.toMatrix_innerₛₗ_apply, Function.locallyFinsuppWithin.toClosedBall_divisor, wInner_one_eq_inner, Matrix.inner_toEuclideanCLM, Matrix.PosSemidef.toLinearMap₂'_zero_iff, contDiffAt_euclidean, innerSLFlip_apply_apply, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, finrank_euclideanSpace, Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero, InnerProductSpace.continuousLinearMapOfBilin_zero, ContinuousLinearMap.toLinearMap_innerSL_apply, ValueDistribution.characteristic_sub_characteristic_inv_le, contDiffOn_euclidean, HasGradientAt.hasFDerivAt, Real.fourier_fderiv, eqOn_iteratedDeriv_cotTerm, HasFDerivWithinAt.norm_sq, LinearMap.tracePositiveLinearMap_apply, Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, Orthonormal.linearIsometryEquiv_symm_apply_single_one, UnitAddTorus.orthonormal_mFourier, Matrix.ofLp_toEuclideanCLM, MDifferentiable.slash, fourierCoeff_toLp, coe_fourierBasis, AddChar.wInner_cWeight_eq_one_iff_eq, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, ModularFormClass.qExpansion_coeff, inner_tmul_eq, hasSum_sq_fourierCoeffOn, torusIntegral_const_mul, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, HasGradientAt.differentiableAt, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, hasSum_mellin_pi_mul, le_radius_cauchyPowerSeries, wInner_const_left, wInner_cWeight_const_left, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, hasStrictFDerivAt_norm_sq, LinearMap.adjoint_toSpanSingleton, hasMellin_one_Ioc, TemperedDistribution.instLineDerivSMulReal, inner_apply, MeasureTheory.Measure.toTemperedDistribution_apply, Complex.analyticOn_iff_differentiableOn, ValueDistribution.characteristic_mul_zero_eventuallyLE, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, ValueDistribution.characteristic_pow_zero, ValueDistribution.characteristic_top_mul_le, norm_wInner_le, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, TemperedDistribution.fourier_lineDerivOp_eq, Matrix.l2_opNNNorm_def, TemperedDistribution.fourier_delta_zero, PeriodPair.order_weierstrassP, MeromorphicNFOn.Gamma, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, ValueDistribution.characteristic_sub_characteristic_inv, EuclideanSpace.basisFun_repr, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, OrthonormalBasis.equiv_apply_euclideanSpace, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, Complex.orthonormalBasisOneI_repr_symm_apply, UnitAddTorus.hasSum_mFourier_series_L2, TemperedDistribution.laplacian_eq_sum, ValueDistribution.isBigO_characteristic_sub_characteristic_inv, HasGradientWithinAt.fderivWithin_apply, TemperedDistribution.instContinuousLineDeriv, Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, wInner_const_right, InnerProductSpace.rankOne_def', Complex.HadamardThreeLines.diffContOnCl_interpStrip, Matrix.IsHermitian.eigenvectorUnitary_apply, Distribution.IsVanishingOn.iteratedLineDerivOp, hasFPowerSeriesOn_cauchy_integral, UpperHalfPlane.contMDiff_denom_zpow, Complex.circleIntegral_div_sub_of_differentiable_on_off_countable, EuclideanSpace.inner_eq_star_dotProduct, DifferentiableOn.hasFPowerSeriesOnBall, OrthonormalBasis.sum_repr_symm, Complex.analyticOn_univ_iff_differentiable, fourierIntegral_gaussian_innerProductSpace, Differentiable.contDiff, InnerProductSpace.innerSL_norm, HurwitzZeta.hurwitzOddFEPair_f₀, ValueDistribution.characteristic_mul_zero_le, Distribution.dsupport_smulLeftCLM_subset, cot_pi_mul_contDiffWithinAt, TemperedDistribution.smulLeftCLM_add, PeriodPair.coeff_weierstrassPSeries, ProbabilityTheory.covarianceBilin_apply_basisFun, hasGradientAt_iff_hasFDerivAt, locallyFinsuppWithin.logCounting_divisor, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, HurwitzZeta.hurwitzOddFEPair_ε, OrthonormalBasis.measurePreserving_repr_symm, EuclideanSpace.piLpCongrLeft_single, hasFDerivWithinAt_euclidean, Matrix.IsHermitian.eigenvectorUnitary_coe, linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero, TemperedDistribution.fourierTransform_apply, MeromorphicOn.circleAverage_log_norm, Matrix.toEuclideanLin_eq_toLin, Matrix.isHermitian_iff_isSymmetric, hasSum_mellin_pi_mul₀, ValueDistribution.characteristic_pow_top, EuclideanSpace.basisFun_inner, UnitAddTorus.hasSum_mFourier_series_of_summable, Real.fourierIntegral_fderiv, InnerProductSpace.toMatrix_rankOne, differentiableAt_euclidean, PeriodPair.hasFPowerSeriesOnBall_weierstrassP, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, harmonic_is_realOfHolomorphic, PeriodPair.weierstrassPSeries_hasSum, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, span_fourierLp_closure_eq_top, circleIntegral.integral_sub_zpow_of_ne, LSeries.iteratedDeriv_alternating, AnalyticAt.cpow, UpperHalfPlane.meromorphicOrderAt_comp_smul, differentiableOn_euclidean, ContinuousLinearMap.adjoint_toSpanSingleton, circleIntegral.integral_smul_const, SchwartzMap.integral_fourier_mul_eq, PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept, wInner_one_const_right, Matrix.ofLp_toEuclideanLin_apply, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, Polynomial.fourierCoeff_toAddCircle_natCast, EuclideanSpace.inner_basisFun_real, innerSLFlip_apply, fourierCoeffOn_of_hasDerivAt_Ioo, InnerProductSpace.toContinuousLinearMap_toDualMap, OrthonormalBasis.repr_symm_single, ValueDistribution.characteristic_zero_mul_eventually_le, innerSL_apply_norm, InnerProductSpace.toDual_apply_eq_toDualMap_apply, PeriodPair.analyticOnNhd_derivWeierstrassP, hasFPowerSeriesOnBall_cuspFunction, tsum_sq_fourierCoeffOn, ModularFormClass.qExpansion_coeff_eq_circleIntegral, MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one, TensorProduct.norm_lid, MeasureTheory.charFun_eq_charFunDual_toDualMap, Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, PeriodPair.meromorphic_weierstrassP, toMatrix_innerSL_apply, TemperedDistribution.fourierMultiplierCLM_apply_apply, PeriodPair.analyticAt_derivWeierstrassPExcept, TemperedDistribution.instFourierInvSMul, HurwitzZeta.hurwitzOddFEPair_g₀, Distribution.dsupport_iteratedLineDerivOp_subset, TemperedDistribution.instFourierInvAdd, UnitAddTorus.hasSum_prod_mFourierCoeff, circleIntegral.circleIntegral_congr_codiscreteWithin, TemperedDistribution.fourierInv_apply, HurwitzZeta.hurwitzOddFEPair_f, fourierCoeff.const_mul, AnalyticOnNhd.sum_divisor_le, Real.tsum_eq_tsum_fourier_of_rpow_decay, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, one_add_cpow_hasFPowerSeriesOnBall_zero, TemperedDistribution.instLineDerivAdd, hasSum_fourier_series_of_summable, inner_gradientWithin_left, TemperedDistribution.instLineDerivSMulComplex, LSeries_analyticOn, HilbertBasis.repr_self, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', ValueDistribution.characteristic_zero_mul_le, Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, SchwartzMap.integral_fourierInv_mul_eq, hasFDerivWithinAt_iff_hasGradientWithinAt, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, Matrix.toEuclideanLin_apply_piLp_toLp, mdifferentiable_jacobiTheta, Orthonormal.orthogonalFamily, Distribution.dsupport_lineDerivOp_subset, PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept, TemperedDistribution.fourierMultiplierCLM_sum, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, SchwartzMap.integral_fourier_smul_eq, HurwitzZeta.hurwitzOddFEPair_k, UpperHalfPlane.contMDiffAt_ofComplex, wInner_one_const_left, ModularForm.holo', ProbabilityTheory.analyticOn_complexMGF, innerSL_apply, OrthonormalBasis.coe_toBasis_repr, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, StrongDual.toLp_apply, OrthonormalBasis.sum_repr, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, DifferentiableOn.analyticOnNhd, hasSum_sq_fourierCoeff, UpperHalfPlane.contMDiffAt_iff, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, Complex.taylorSeries_eq_on_eball', UnitAddTorus.mFourierBasis_repr, Function.Periodic.contDiff_qParam, Complex.analyticOnNhd_iff_differentiableOn, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, fourierBasis_repr, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt, MeasureTheory.BoundedContinuousFunction.inner_toLp, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, OrthonormalBasis.coe_toBasis_repr_apply, UpperHalfPlane.mdifferentiable_coe, TemperedDistribution.isVanishingOn_delta, OrthonormalBasis.coe_equiv_euclideanSpace, PeriodPair.weierstrassPExceptSeries_hasSum, ModularFormClass.analyticAt_cuspFunction_zero, Complex.HadamardThreeLines.scale_diffContOnCl, TemperedDistribution.lineDerivOp_apply_apply, Complex.HadamardThreeLines.diffContOnCl_invInterpStrip, signedDist_apply, UnitAddTorus.hasSum_mFourier_series_apply_of_summable, EuclideanSpace.inner_toLp_toLp, UnitAddTorus.hasSum_sq_mFourierCoeff, TemperedDistribution.lineDerivOp_fourierInv_eq, HurwitzZeta.hurwitzOddFEPair_g, HasFDerivAt.hasGradientAt, Complex.circleTransformDeriv_bound, Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable, Matrix.IsHermitian.eigenvectorUnitary_transpose_apply, analyticAt_clog, AddChar.linearIndependent, InnerProductSpace.harmonic_is_realOfHolomorphic_univ, ModularFormClass.holo, circleIntegral.integral_sub_center_inv, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, wInner_cWeight_const_right, TemperedDistribution.smulLeftCLM_sum, fourierCoeff_liftIoc_eq, TemperedDistribution.instContinuousFourierInv, Complex.one_add_cpow_hasFPowerSeriesOnBall_zero, AddChar.wInner_cWeight_eq_boole, EuclideanSpace.restrict₂_apply, EuclideanSpace.inner_single_right, TemperedDistribution.fourier_apply, hasMellin_cpow_Ioc, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, tsum_sq_fourierCoeff, Submodule.orthogonal_eq_inter, VectorFourier.integral_fourierIntegral_smul_eq_flip, SchwartzMap.coe_apply, DifferentiableOn.analyticAt, fderiv_norm_rpow, Matrix.toEuclideanLin_eq_toLin_orthonormal, AnalyticWithinAt.clog, Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero, UpperHalfPlane.mdifferentiableAt_iff, OrthonormalBasis.coe_singleton, fourierCoeffOn_of_hasDerivAt, PeriodPair.analyticOnNhd_weierstrassPExcept, DiffContOnCl.hasFPowerSeriesOnBall, TemperedDistribution.smulLeftCLM_smul, HasGradientAt.hasDerivAt, ArithmeticFunction.iteratedDeriv_LSeries_alternating, InnerProductSpace.continuousLinearMapOfBilin_apply, Matrix.cstar_norm_def, Real.tsum_eq_tsum_fourierIntegral, SchwartzMap.tsum_eq_tsum_fourierIntegral, inner_matrix_row_row, ValueDistribution.characteristic_top_mul_eventually_le, HasGradientAt.fderiv_apply, TemperedDistribution.derivCLM_apply_apply, Complex.taylorSeries_eq_of_entire', Meromorphic.Gamma, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq, inner_gradient_left, innerSL_apply_coe, ProbabilityTheory.analyticOnNhd_complexMGF, MeasureTheory.ContinuousMap.inner_toLp, gradient_eq_deriv, TemperedDistribution.fourierTransformInv_apply, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, UpperHalfPlane.contMDiff_smul, TensorProduct.nnnorm_lid, eqOn_iteratedDerivWithin_cotTerm_integerComplement, Matrix.IsHermitian.mulVec_eigenvectorBasis, Matrix.l2_opNorm_def, wInner_nonneg, Matrix.toEuclideanLin_toLp, UpperHalfPlane.contMDiff_denom, norm_innerSL_le, BoundedContinuousFunction.separatesPoints_charPoly, Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, UnitAddTorus.span_mFourierLp_closure_eq_top, PeriodPair.analyticOnNhd_weierstrassP, UpperHalfPlane.mdifferentiable_denom_zpow, HasGradientWithinAt.hasFDerivWithinAt, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, Pi.orthonormalBasis_repr, MeromorphicOn.Gamma, Polynomial.fourierCoeff_toAddCircle, Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, HasGradientAtFilter.hasDerivAtFilter, inner_gradient_right, UpperHalfPlane.mdifferentiable_iff, Real.fourierIntegral_iteratedFDeriv, Complex.analyticAt_iff_eventually_differentiableAt, finrank_euclideanSpace_fin, fourierCoeffOn_of_hasDeriv_right, OrthonormalBasis.repr_reindex, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, ContinuousLinearMap.adjoint_innerSL_apply, Distribution.IsVanishingOn.lineDerivOp, UpperHalfPlane.mdifferentiableAt_ofComplex, fourier_gaussian_pi, Real.fourier_smul_convolution_eq, MeasureTheory.condExpL2_const_inner, TemperedDistribution.laplacianCLM_apply, Complex.taylorSeries_eq_on_emetric_ball', fourierCoeff_liftIco_eq, contDiff_euclidean, fderiv_norm_sq_apply, OrthonormalBasis.tensorProduct_repr_tmul_apply, circleIntegral.integral_const_mul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, inner_eq_wInner_one, Differentiable.analyticAt, fderiv_norm_sq, ValueDistribution.characteristic_mul_top_eventuallyLE, Complex.one_div_sub_hasFPowerSeriesOnBall_zero, ContinuousLinearMap.innerSL_apply_comp, TensorProduct.lidIsometry_symm_apply, fourierIntegral_gaussian_pi', ContinuousLinearMap.toSesqForm_apply_norm_le, HilbertBasis.hasSum_repr_symm, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, TemperedDistribution.smulLeftCLM_apply_apply, hasSum_mellin_pi_mul_sq, inner_matrix_col_col, BoundedContinuousFunction.char_mem_charPoly, SchwartzMap.tsum_eq_tsum_fourier, norm_jacobiTheta₂_term_fderiv_le, UpperHalfPlane.mdifferentiable_smul, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, DifferentiableOn.analyticOn, hasStrictFDerivAt_euclidean, fourierCoeff_fourier
toInnerProductSpaceReal 📖	CompOp	1469 math math: Real.hasDerivAt_fourier, ProbabilityTheory.variance_eq_integral, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, MeasureTheory.Integrable.integral_norm_prod_right, MeasureTheory.mulEquivHaarChar_smul_integral_map, Bundle.ContMDiffRiemannianMetric.isVonNBounded, ProbabilityTheory.integral_cauchyPDFReal_eq_one, Polynomial.mahlerMeasure_def_of_ne_zero, MeasureTheory.supermartingale_of_setIntegral_succ_le, Bundle.ContMDiffRiemannianMetric.contMDiff, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable, MonotoneOn.intervalIntegral_slope_le, Distribution.delta_apply, ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul, ProbabilityTheory.isGaussian_iff_gaussian_charFun, exists_contMDiffMap_zero_one_of_isClosed, InformationTheory.integral_llr_add_mul_log_nonneg, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, mellin_eq_fourier, integral_cos, ProbabilityTheory.condDistrib_ae_eq_condExp, Real.hasFDerivAt_fourierChar_neg_bilinear_left, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, ConvexOn.map_condExp_le_univ, Function.hasTemperateGrowth_inner_right, NumberField.Units.finrank_eq_rank, ValueDistribution.proximity_zero, Real.fourierCoeff_tsum_comp_add, tendsto_tsum_div_pow_atTop_integral, MeasureTheory.taylor_charFun_two, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, ZSpan.volume_real_fundamentalDomain, Complex.areaForm, Real.tsum_eq_tsum_fourier, Real.hasDerivAt_sigmoid, ProbabilityTheory.analyticOn_mgf, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, Matrix.IsHermitian.det_abs, ProbabilityTheory.condIndep_iff, deriv_abs, integral_sin_mul_cos₂, MeasureTheory.Submartingale.sum_mul_sub', ProbabilityTheory.covarianceBilinDual_apply', MeasureTheory.toReal_rnDeriv_trim, ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq, contDiffAt_norm_smul_iff, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, intervalIntegral.mul_integral_comp_mul_sub, AnalyticOn.im_ofReal, AbsolutelyContinuousOnInterval.integral_deriv_eq_sub, ContDiff.sigmoid, intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, Polynomial.Chebyshev.integral_measureT_eq_integral_cos, integral_const_on_unit_interval, integral_exp_mul_Iic, MeasureTheory.submartingale_iff_expected_stoppedValue_mono, ZLattice.covolume_eq_det_inv, ProbabilityTheory.covarianceBilinDual_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, MeasureTheory.integral_fintype_prod_volume_eq_pow, Real.fderiv_fourierChar_neg_bilinear_right_apply, ProbabilityTheory.isGaussian_multivariateGaussian, MeasureTheory.iteratedDeriv_charFun_zero, ConvexOn.map_set_average_le, intervalIntegral.fderiv_integral_of_tendsto_ae, flip_innerSL_real, LipschitzWith.memLp_lineDeriv, AnalyticOnNhd.re_ofReal, SmoothPartitionOfUnity.contMDiffAt_finsum, differentiableWithinAt_abs_pos, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, LipschitzWith.ae_lineDeriv_sum_eq, Orientation.inner_mul_inner_add_areaForm_mul_areaForm, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right, Orientation.areaForm_le, DifferentiableWithinAt.norm, det_fderivPolarCoordSymm, MeasureTheory.smul_le_stoppedValue_hittingBtwn, SmoothPartitionOfUnity.locallyFinite, ProbabilityTheory.covarianceBilin_multivariateGaussian, exists_smooth_one_nhds_of_subset_interior, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, SmoothPartitionOfUnity.nonneg, hasDerivAt_bernoulliFun, Orientation.volumeForm_neg_orientation, ProbabilityTheory.sum_prob_mem_Ioc_le, MeasureTheory.pdf.integral_mul_eq_integral, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le, ProbabilityTheory.uncenteredCovarianceBilin_apply, contMDiff_neg_sphere, not_differentiableAt_norm_zero, circleAverage_log_norm_sub_const₁, BoxIntegral.unitPartition.mem_smul_span_iff, exists_eq_const_mul_intervalIntegral_of_nonneg, ContDiffBump.integral_normed, MeasureTheory.integral_fintype_prod_eq_prod, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, HasGradientAt.hasDerivAt', SmoothBumpCovering.exists_immersion_euclidean, AnalyticOnNhd.circleAverage_log_norm, DifferentiableAt.sigmoid, IsOpen.exists_msmooth_support_eq, IsOpen.exists_smooth_support_eq, SmoothPartitionOfUnity.locallyFinite', Real.rpow_eq_const_mul_integral, interval_average_eq_div, Bundle.RiemannianMetric.isVonNBounded, ProbabilityTheory.setIntegral_condCDF, integral_pow, fourier_gaussian_pi', ProbabilityTheory.integral_continuousLinearMap_gaussianReal, Differentiable.fderiv_norm_rpow, integral_log_sin_zero_pi_div_two, lintegral_fderiv_lineMap_eq_edist, exists_eq_interval_average_of_noAtoms, TopologicalGroup.IsSES.integral_inducedMeasure, MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div, ConvexOn.set_average_mem_epigraph, MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part, MeasureTheory.AECover.integral_eq_of_tendsto_of_nonneg_ae, signedDist_right_congr, StrictConcaveOn.ae_eq_const_or_lt_map_average, intervalIntegral.integral_ofReal, ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul, ContDiffOn.inner, MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul, integral_exp, integral_inv_of_pos, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, Module.Basis.parallelepiped_basisFun, SchwartzMap.laplacianCLM_eq, monomial_has_deriv_aux, MeasureTheory.hasFiniteIntegral_prod_iff', Real.vector_fourierIntegral_eq_integral_exp_smul, Real.fourier_real_eq_integral_exp_smul, ProbabilityTheory.cdf_paretoMeasure_eq_integral, differentiableWithinAt_abs, ProbabilityTheory.ae_eq_integral_of_variance_eq_zero, LocallyBoundedVariationOn.ae_differentiableWithinAt, integral_sin_pow_three, Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, circleAverage_log_norm_sub_const_of_mem_closedBall, hasStrictDerivAt_abs_pos, hasDerivWithinAt_abs_pos, HasFDerivAt.norm_sq, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, MeasureTheory.Submartingale.sum_upcrossingStrat_mul, analyticOnNhd_circleMap, antideriv_bernoulliFun, NumberField.mixedEmbedding.commMap_apply_of_isComplex, differentiableAt_sigmoid, Real.fourier_deriv, ProbabilityTheory.IsCondKernelCDF.integral, intervalIntegral.integral_mono_on, abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure, MeasureTheory.L2.inner_def, Orientation.volumeForm_map, Icc_isBoundaryPoint_bot, Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero, deriv_abs_neg, ProbabilityTheory.moment_one, integral_exp_neg_mul_rpow, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, MeasureTheory.convolution_tendsto_right, DifferentiableWithinAt.abs_of_pos, Polynomial.Chebyshev.integral_measureT, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, intervalIntegral.integral_div, HarmonicAt.analyticAt_complex_partial, InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul, integral_sin_pow_pos, signedDist_left_congr, Complex.integral_rpow_mul_exp_neg_rpow, OrthonormalBasis.measurePreserving_repr, InformationTheory.leftDeriv_klFun_one, integral_Ioi_rpow_of_lt, exists_smooth_tsupport_subset, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, signedDist_triangle, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn, AnalyticOn.sigmoid, integral_bernoulliFun, enorm_fderiv_norm_rpow_le, HarmonicOnNhd.circleAverage_eq, LocallyBoundedVariationOn.ae_differentiableAt, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, MeasureTheory.Submartingale.stoppedValue_leastGE, MonotoneOn.intervalIntegrable_deriv, MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff, Real.Icc_mem_vitaliFamily_at_left, Orientation.abs_volumeForm_apply_of_orthonormal, ContDiffBump.normed_def, signedDist_linear_apply_apply, BoxIntegral.hasIntegral_GP_pderiv, setIntegral_Ioi_zero_rpow, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg, SchwartzMap.norm_toLp_one, integral_rpow_mul_exp_neg_rpow, NumberField.mixedEmbedding.negAt_apply_snd, MeasureTheory.measure_lt_one_eq_integral_div_gamma, MeasureTheory.setIntegral_prod_mul, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos', Real.one_add_rpow_hasFPowerSeriesOnBall_zero, Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous, VectorFourier.fourierPowSMulRight_eq_comp, AnalyticAt.sigmoid', MeasureTheory.charFunDual_eq_charFun_map_one, MeasureTheory.integral_fintype_prod_eq_pow, mfderivWithin_projIcc_one, intervalIntegral.integral_pos_iff_support_of_nonneg_ae', integral_cos_pow, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, AnalyticAt.harmonicAt_im, ProbabilityTheory.integral_stieltjesOfMeasurableRat, ProbabilityTheory.variance_of_integral_eq_zero, MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, ProbabilityTheory.IndepFun.integral_comp_mul_comp, Euclidean.closedBall_eq_image, MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo, NumberField.mixedEmbedding.negAt_preimage, InformationTheory.not_differentiableWithinAt_klFun_Iio_zero, ProbabilityTheory.charFun_multivariateGaussian, intervalIntegral.integral_mono_ae_restrict, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, BoxIntegral.unitPartition.integralSum_eq_tsum_div, InformationTheory.toReal_klDiv_eq_integral_klFun, Quaternion.linearIsometryEquivTuple_symm_apply, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, MeasureTheory.SignedMeasure.singularPart_smul, ProbabilityTheory.covarianceBilin_apply_basisFun_self, MeasureTheory.charFun_apply_real, Orientation.areaForm_to_volumeForm, Icc_isInteriorPoint_interior, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, signedDist_le_dist, Orientation.areaForm_neg_orientation, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, Function.Periodic.sInf_add_zsmul_le_integral_of_pos, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, Monotone.ae_differentiableAt, ProbabilityTheory.iCondIndep_iff, ProbabilityTheory.centralMoment_one', MeasureTheory.integral_fin_nat_prod_volume_eq_prod, ConvexOn.map_condExp_le_of_finiteDimensional, MeasureTheory.condExpL2_indicator_ae_eq_smul, Differentiable.abs, mfderivWithin_comp_projIcc_one, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, HarmonicContOnCl.circleAverage_eq, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, SmoothPartitionOfUnity.sum_finsupport', SchwartzMap.smulLeftCLM_real_smul, ProbabilityTheory.variance_le_sub_mul_sub, ContDiffBump.measure_closedBall_div_le_integral, signedDist_apply_apply, integral_sin_sq, SchwartzMap.integral_norm_sq_fourier, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, ProbabilityTheory.gaussianReal_map_continuousLinearMap, Manifold.pathELength_def, EuclideanSpace.volume_closedBall_fin_three, IccLeftChart_extend_interior_pos, taylor_integral_remainder_of_absolutelyContinuous, Orientation.areaForm_swap, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Bundle.ContinuousRiemannianMetric.symm, MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq, InformationTheory.tendsto_rightDeriv_klFun_atTop, intervalIntegral.integral_mono, MeasureTheory.Integrable.integral_norm_condDistrib_map, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, hasDerivAt_abs_neg, MeasureTheory.integral_mul_upcrossingsBefore_le_integral, intervalIntegral.integral_mono_interval, MeasureTheory.condExp_smul_of_aestronglyMeasurable_right, Matrix.PosSemidef.det_sqrt, DifferentiableWithinAt.dist, hasDerivWithinAt_abs, contDiff_circleMap, intervalIntegral.integral_mono_on_of_le_Ioo, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, BoundedVariationOn.intervalIntegrable_deriv, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem, VectorFourier.hasFDerivAt_fourierIntegral, MeasureTheory.Integrable.tendsto_eLpNorm_condExp, MeasureTheory.convolution_precompR_apply, SchwartzMap.compSubConstCLM_apply, ProbabilityTheory.condIndepSets_singleton_iff, VectorFourier.fourierIntegral_iteratedFDeriv, MonotoneOn.sum_le_integral, InformationTheory.hasDerivAt_klFun, MeasureTheory.setIntegral_condExpL2_indicator, contMDiff_coe_sphere, integral_cos_pow_aux, BoundedContinuousFunction.mem_charPoly, intervalIntegral.abs_intervalIntegral_eq, InformationTheory.toReal_klDiv, BoundedContinuousFunction.charAlgHom_apply, ae_differentiableAt_norm, IsOpen.exists_contMDiff_support_eq_aux, NumberField.Units.instZLattice_unitLattice, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, ProbabilityTheory.tendsto_integral_truncation, Orientation.volumeForm_zero_pos, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf', fourierIntegral_gaussian_pi, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, ProbabilityTheory.complexMGF_mul_I, MeasureTheory.condExp_mul_of_aestronglyMeasurable_right, DifferentiableAt.fderiv_norm_self, NumberField.Units.span_basisOfIsMaxRank, ConcaveOn.condExp_map_le, MeasureTheory.Submartingale.sum_mul_sub, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, ProbabilityTheory.Kernel.martingale_densityProcess, AnalyticAt.log, Complex.GammaIntegral_ofReal, mellinInv_eq_fourierIntegralInv, HasDerivWithinAt.norm_sq, HasGradientAtFilter.hasDerivAtFilter', MonotoneOn.integral_le_sum_Ico, PiLp.volume_preserving_toLp, InnerProductGeometry.norm_toLp_symm_crossProduct, SmoothPartitionOfUnity.contDiffAt_finsum, intervalIntegral.intervalIntegral_pos_of_pos, Chebyshev.integral_one_div_log_sq_isBigO, NumberField.Units.basisOfIsMaxRank_apply, Complex.integral_exp_neg_rpow, taylor_mean_remainder_lagrange_iteratedDeriv, MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, ProbabilityTheory.analyticAt_mgf, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, orthonormalBasis_one_dim, integral_le_sum_mul_Ico_of_antitone_monotone, LipschitzWith.ae_lineDifferentiableAt, InformationTheory.leftDeriv_klFun, integral_bernoulliFun_eq_zero, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, MeasureTheory.Integrable.tendsto_ae_condExp, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, MeasureTheory.Integrable.integral_norm_comp, ProbabilityTheory.differentiableAt_mgf, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable, analyticOn_log, BumpCovering.contMDiff_toPartitionOfUnity, analyticOnNhd_log, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, ProbabilityTheory.iteratedDeriv_mgf, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf, norm_cauchyPowerSeries_le, sum_mul_eq_sub_integral_mul', ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le, Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, mellinInv_eq_fourierInv, ODE.contDiffOn_nat_picard_Icc, Metric.exists_smooth_forall_closedBall_subset, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, ContDiffBump.convolution_tendsto_right, ContDiffAt.contDiffAt_norm_smul, Real.fourier_real_eq, intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt, hasDerivAt_abs_rpow, signedDist_eq_zero_of_orthogonal, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, ZSpan.volume_fundamentalDomain, ProbabilityTheory.covarianceBilin_zero, VectorFourier.differentiable_fourierIntegral, MeasureTheory.condExp_mul_of_stronglyMeasurable_right, analyticOnNhd_sigmoid, ProbabilityTheory.integral_truncation_eq_intervalIntegral, ProbabilityTheory.condExpKernel_ae_eq_condExp', Real.deriv_Gamma_nat, ContDiff.norm_rpow, Distribution.delta_eq_zero_of_notMem, Real.fourierIntegral_convergent_iff', Bundle.ContMDiffRiemannianMetric.symm, MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul, ProbabilityTheory.analyticOnNhd_cgf, MeasureTheory.lintegral_nnnorm_condExpL2_le, SmoothPartitionOfUnity.le_one, Monotone.ae_hasDerivAt, ProbabilityTheory.IsCondKernelCDF.setIntegral, AffineSubspace.signedInfDist_eq_signedDist_of_mem, EuclideanSpace.volume_closedBall_fin_two, Affine.Simplex.signedInfDist_apply_self, VectorFourier.iteratedFDeriv_fourierIntegral, exists_contMDiffMap_zero_one_nhds_of_isClosed, ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le, intervalIntegral.integral_deriv_comp_mul_deriv', Real.one_div_one_sub_hasFPowerSeriesOnBall_zero, ContDiffBump.normed_convolution_eq_right, ProbabilityTheory.gaussianReal_map_linearMap, HasDerivWithinAt.inner, AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub, MeasureTheory.toReal_condLExp, BoxIntegral.integral_nonneg, DifferentiableAt.inner, HarmonicAt.differentiableAt_complex_partial, ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul, IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, Real.fourierIntegral_iteratedDeriv, MeasureTheory.hasFDerivAt_convolution_right_with_param, ProbabilityTheory.IsGaussian.charFun_eq', ProbabilityTheory.covarianceBilinDual_eq_covariance, signedDist_zero, SchwartzMap.postcompCLM_apply, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, EulerSine.sin_pi_mul_eq, integral_exp_Iic, Chebyshev.primeCounting_eq_theta_div_log_add_integral, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, InformationTheory.integral_llr_add_sub_measure_univ_nonneg, MeasureTheory.Integrable.integral_norm_prod_left, HasCompactSupport.hasFDerivAt_convolution_right, frontier_range_modelWithCornersEuclideanHalfSpace, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul, ProbabilityTheory.covarianceBilinDual_zero, contDiff_bernoulliFun, SchwartzMap.seminorm_le_bound', MeasureTheory.submartingale_of_setIntegral_le_succ, HasFDerivWithinAt.inner, EuclideanSpace.instIsManifoldSphere, MeasureTheory.tendsto_sum_indicator_atTop_iff, Orientation.abs_volumeForm_apply_of_pairwise_orthogonal, DifferentiableWithinAt.abs, MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq, circleAverage_log_norm_sub_const₀, ProbabilityTheory.condIndepSet_iff, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable, ProbabilityTheory.differentiableOn_mgf, contDiffOn_abs, MeasureTheory.Integrable.integral_norm_condExpKernel, dist_integral_mulExpNegMulSq_comp_le, SmoothBumpFunction.contMDiffAt, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le, ProbabilityTheory.complexMGF_id_mul_I, ProbabilityTheory.map_pi_eq_stdGaussian, Real.one_div_sub_hasFPowerSeriesOnBall_zero, ProbabilityTheory.integral_id_multivariateGaussian, ContDiff.euclidean_dist, MeasureTheory.condExp_mul_of_aestronglyMeasurable_left, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, Bundle.ContMDiffRiemannianMetric.pos, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf', signedDist_triangle_left, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, IsContMDiffRiemannianBundle.exists_contMDiff, sum_Ico_le_integral_of_le, integral_sin_pow_mul_cos_pow_odd, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul', integral_rpow_mul_exp_neg_mul_rpow, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, ProbabilityTheory.integral_gaussianPDFReal_eq_one, contMDiff_subtype_coe_Icc, ProperCone.innerDual_singleton, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, InformationTheory.integral_klFun_rnDeriv, differentiable_inner, intervalIntegral.abs_integral_mono_interval, Polynomial.Chebyshev.integral_eq_sumZeroes, hasFDerivAt_integral_of_dominated_loc_of_lip', integral_id, ExistsContDiffBumpBase.u_int_pos, ContDiffOn.abs, Real.differentiableAt_Gamma, Real.pow_mul_norm_iteratedFDeriv_fourier_le, NumberField.mixedEmbedding.mem_span_latticeBasis, ProbabilityTheory.evariance_eq_lintegral_ofReal, ProbabilityTheory.integral_condVar_add_variance_condExp, ContDiffWithinAt.norm_sq, Function.hasTemperateGrowth_norm_sq, ProbabilityTheory.analyticOn_cgf, Real.zero_at_infty_fourierIntegral, ProbabilityTheory.covarianceBilin_comm, intervalIntegral.integral_congr_codiscreteWithin, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, InformationTheory.klDiv_of_ac_of_integrable, gradient_eq_deriv', MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, MonotoneOn.intervalIntegrable_slope, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, SchwartzMap.compCLMOfAntilipschitz_apply, SchwartzMap.fourierInv_apply_eq, SchwartzMap.smulRightCLM_apply_apply, Real.differentiableOn_Gamma_Ioi, MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux, ProbabilityTheory.analyticAt_cgf, InformationTheory.klDiv_def, MeasureTheory.L2.inner_indicatorConstLp_one, taylor_mean_remainder, abs_wInner_le, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, fderiv_norm_smul_neg, ExistsContDiffBumpBase.u_exists, Real.fourierIntegral_real_eq_integral_exp_smul, Real.deriv_fourierIntegral, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae, dense_differentiableAt_norm, AntitoneOn.sum_le_integral_Ico, MeasureTheory.submartingale_of_setIntegral_le, SchwartzMap.postcompCLM_postcompCLM, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, ContDiff.norm_sq, MonotoneOn.intervalIntegral_deriv_mem_uIcc, NumberField.mixedEmbedding.volume_preserving_negAt, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, ProbabilityTheory.condVar_of_stronglyMeasurable, SmoothPartitionOfUnity.sum_eq_one', integral_sin_mul_cos₁, MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous, ProbabilityTheory.iCondIndepSets_singleton_iff, NumberField.mixedEmbedding.negAt_apply_isComplex, Real.integral_rpowIntegrand₀₁_one_pos, ProbabilityTheory.hasFiniteIntegral_compProd_iff', ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg, Matrix.inner_toEuclideanCLM, integral_sin_pow_aux, integral_comp_abs, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, integral_div_sq_add_sq, SmoothPartitionOfUnity.mem_finsupport, Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, IsOpen.exists_contMDiff_support_eq, ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral, Matrix.instNonnegSpectrumClass, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, DifferentiableAt.norm_sq, ProbabilityTheory.sum_variance_truncation_le, Orientation.areaForm'_apply, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound, signedDist_smul_of_pos, Distribution.mapCLM_apply, IsContinuousRiemannianBundle.exists_continuous, MonotoneOn.sum_le_integral_Ico, ProbabilityTheory.condExp_set_generateFrom_singleton, MeasureTheory.dist_convolution_le, intervalIntegral.integral_hasStrictFDerivAt, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, signedDist_lineMap_lineMap, mfderiv_coe_sphere_injective, ProbabilityTheory.variance_eq_sub, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, NumberField.Units.regOfFamily_of_isMaxRank, intervalIntegral.inv_mul_integral_comp_add_div, analyticAt_sigmoid, contDiffAt_norm, tendsto_integral_mul_one_add_inv_smul_sq_pow, AnalyticOnNhd.circleAverage_log_norm_of_ne_zero, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, PiLp.volume_preserving_ofLp, integral_sin_pow_even_mul_cos_pow_even, ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet, signedDist_vadd_left_swap, MeasureTheory.integrable_prod_iff, SchwartzMap.compSubConstCLM_zero, sum_mul_Ico_le_integral_of_monotone_antitone, HasFDerivWithinAt.norm_sq, ProbabilityTheory.meas_ge_le_variance_div_sq, differentiableAt_abs_neg, ProbabilityTheory.isGaussian_gaussianReal, norm_fderiv_norm_rpow_le, integral_inner, deriv_abs_zero, VectorFourier.fderiv_fourierIntegral, InnerProductGeometry.norm_ofLp_crossProduct, hasStrictDerivAt_abs, Bundle.RiemannianMetric.symm, MeasureTheory.integral_charFun_Icc, ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone, ContDiffWithinAt.dist, sum_mul_eq_sub_integral_mul₀', ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg, Differentiable.sigmoid, AffineSubspace.signedInfDist_eq_const_of_mem, MeasureTheory.mul_le_integral_rnDeriv_of_ac, intervalIntegral.inv_mul_integral_comp_sub_div, MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le, Function.Periodic.tendsto_atBot_intervalIntegral_of_pos', AEStronglyMeasurable.norm_condExp_le, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, DifferentiableOn.norm_sq, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, Differentiable.norm_rpow, intervalIntegral.integral_mono_ae, ProbabilityTheory.variance_continuousLinearMap_gaussianReal, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, ProbabilityTheory.covariance_eq_sub, MeasureTheory.integrable_conv_iff, signedDist_vadd_right, hasSum_sq_fourierCoeffOn, Real.circleAverage_mono_on_of_le_circle, ProbabilityTheory.strong_law_aux6, MeasureTheory.tendsto_sum_indicator_atTop_iff', MeasureTheory.integral_prod_mul, contDiff_norm_sq, tendsto_integral_mulExpNegMulSq_comp, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, intervalAverage_congr_codiscreteWithin, Polynomial.logMahlerMeasure_def, deriv_abs_pos, ProbabilityTheory.hasFPowerSeriesAt_mgf, Complex.integral_exp_neg_mul_rpow, MeasureTheory.smul_le_stoppedValue_hitting, MeasureTheory.convolution_mono_right_of_nonneg, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, MeasureTheory.Measure.integrable_compProd_iff, ContDiff.inner, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae, ProbabilityTheory.covarianceBilin_self_nonneg, DifferentiableOn.abs, HasDerivAt.norm_sq, ProbabilityTheory.integral_linearMap_gaussianReal, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, exists_msmooth_support_eq_eq_one_iff, Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure, MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one, ProbabilityTheory.condIndepSets_iff, MeasureTheory.Submartingale.stoppedProcess, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', MeasureTheory.rnDeriv_trim, integral_inv_of_neg, ProbabilityTheory.covarianceBilinDual_self_eq_variance, ProbabilityTheory.iCondIndepSet_iff, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, Orientation.areaForm_comp_linearIsometryEquiv, hasStrictFDerivAt_norm_sq, SmoothPartitionOfUnity.coe_finsupport, ConcaveOn.le_map_integral, Emetric.exists_contMDiffMap_forall_closedBall_subset, ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, ProbabilityTheory.condVar_ae_le_condExp_sq, MDifferentiableOn.inner_bundle, intervalIntegral.integral_comp_mul_deriv, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul, ProbabilityTheory.Kernel.setIntegral_densityProcess, differentiableAt_norm_smul, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real, AntitoneOn.integral_le_sum_Ico, MeasureTheory.setIntegral_abs_condExp_le, Metric.exists_contMDiffMap_forall_closedBall_subset, ProbabilityTheory.IndepFun.integral_fun_comp_mul_comp, Differentiable.norm_sq, exists_msmooth_zero_iff_one_iff_of_isClosed, ConcaveOn.set_average_mem_hypograph, norm_wInner_le, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real, TopologicalAddGroup.IsSES.integrate_mono, ProbabilityTheory.covarianceBilinDual_self_nonneg, IccLeftChart_extend_bot, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, ContDiffBump.measure_closedBall_le_integral, ProbabilityTheory.Kernel.integral_densityProcess, MeasureTheory.Integrable.integral_eq_integral_meas_le, MeasurableEmbedding.gaussianReal_comap_apply, SmoothPartitionOfUnity.finsum_smul_mem_convex, intervalIntegral.mul_integral_comp_add_mul, signedDist_lineMap_left, ProbabilityTheory.covarianceBilin_real_self, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, Real.fourier_iteratedDeriv, HarmonicAt.analyticAt, integral_univ_inv_one_add_sq, MeasureTheory.Integrable.integral_norm_compProd, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, SmoothPartitionOfUnity.sum_le_one', ValueDistribution.characteristic_sub_characteristic_inv, NumberField.mixedEmbedding.span_latticeBasis, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, integral_exp_neg_rpow, AnalyticWithinAt.re_ofReal, Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay, InformationTheory.klDiv_eq_integral_klFun, VectorFourier.fourierSMulRight_apply, MeasureTheory.Integrable.integral_eq_integral_meas_lt, MeasureTheory.tendsto_ae_condExp, ProbabilityTheory.evariance_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, integral_inv, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ContMDiffOn.inner_bundle, SmoothPartitionOfUnity.sum_nonneg, intervalIntegral.abs_integral_le_integral_abs, Manifold.riemannianEDist_def, Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, tendsto_sum_mul_atTop_nhds_one_sub_integral₀, AnalyticAt.sigmoid, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae', signedDist_anticomm, Real.taylor_tendsto, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, Orientation.areaForm_comp_rightAngleRotation, modelWithCornersEuclideanHalfSpace_zero, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, differentiableWithinAt_abs_neg, sum_mul_eq_sub_integral_mul₁, ContDiffAt.norm_sq, ProbabilityTheory.iteratedDeriv_mgf_zero, ProbabilityTheory.moment_truncation_eq_intervalIntegral, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, ProbabilityTheory.cdf_expMeasure_eq_integral, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup, MeasureTheory.rnDeriv_ae_eq_condExp, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, MeasureTheory.Measure.haarScalarFactor_eq_integral_div, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, ProbabilityTheory.hasFiniteIntegral_comp_iff', ProbabilityTheory.covarianceOperator_inner, mellin_eq_fourierIntegral, hasStrictDerivAt_abs_neg, MDifferentiableWithinAt.inner_bundle, Orientation.inner_rightAngleRotation_left, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, DifferentiableWithinAt.abs_of_neg, integral_cos_pow_three, HasFDerivAt.inner, intervalIntegral.integral_comp_mul_deriv_of_deriv_nonneg, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, integral_one_div_of_pos, ProbabilityTheory.covarianceBilin_apply_pi, ProbabilityTheory.deriv_mgf, ExistsContDiffBumpBase.u_smooth, intervalIntegral.intervalIntegral_pos_of_pos_on, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', ProbabilityTheory.integral_strongDual_stdGaussian, ProbabilityTheory.condExpKernel_ae_eq_condExp, ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub, signedDist_triangle_right, ProbabilityTheory.hasFiniteIntegral_comp_iff, InformationTheory.integral_llr_compProd_eq_add, contMDiffWithinAt_comp_projIcc_iff, Orientation.inner_mul_areaForm_sub', hasFDerivAt_polarCoord_symm, MeasureTheory.dist_convolution_le', MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul, AnalyticWithinAt.im_ofReal, ProbabilityTheory.HasGaussianLaw.charFun_map_eq, ODE.contDiffOn_comp, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp, abs_signedDist_eq_dist_iff_vsub_mem_span, Real.iteratedDeriv_fourier, ProbabilityTheory.Kernel.integral_density, intervalIntegral.integral_comp_mul_deriv''', Real.eulerMascheroniConstant_eq_neg_deriv, EuclideanSpace.volume_ball_fin_three, ProbabilityTheory.IsGaussian.integral_dual, Orientation.abs_areaForm_le, IsOpen.exists_msmooth_support_eq_aux, SchwartzMap.norm_toLp', integral_log_sin_zero_pi, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, intervalIntegral.integral_pos_iff_support_of_nonneg_ae, MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, MeasureTheory.Integrable.integral_norm_condDistrib, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, SchwartzMap.compSubConstCLM_comp, signedDist_neg, ProbabilityTheory.covarianceBilin_apply_basisFun, exists_contMDiff_zero_iff_one_iff_of_isClosed, ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, integral_inv_sq_add_sq, NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single, ProbabilityTheory.setIntegral_preCDF_fst, NumberField.mixedEmbedding.negAt_symm, MeasureTheory.iteratedDeriv_charFun, VectorFourier.contDiff_fourierIntegral, ConcaveOn.le_map_average, ProbabilityTheory.integrable_compProd_iff, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left, ProbabilityTheory.variance_dual_stdGaussian, Polynomial.sum_sq_norm_coeff_eq_circleAverage, ContDiffBump.contDiff_normed, integral_rpow, AnalyticAt.harmonicAt_re, ProbabilityTheory.iCondIndepSets_iff, Diffeology.isPlot_iff_contDiff, signedDist_vsub_self_rev, ODE.contDiffOn_enat_picard_Icc, InformationTheory.toReal_klDiv_of_measure_eq, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae, contDiffAt_inner, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, OrthonormalBasis.measurePreserving_repr_symm, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, norm_fderiv_norm, MeasureTheory.measureReal_abs_gt_le_integral_charFun, DifferentiableOn.inner, integral_exp_neg_Ioi, Differentiable.inner, signedDist_linear_apply, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, oneTangentSpaceIcc_def, ProbabilityTheory.HasSubgaussianMGF.measureReal_le_le_exp, Real.abs_circleAverage_le_circleAverage_abs, IccRightChart_extend_top_mem_frontier, NumberField.mixedEmbedding.volume_negAt_plusPart, InnerProductSpace.laplacianWithin_eq_iteratedDerivWithin_real, ProbabilityTheory.integral_truncation_le_integral_of_nonneg, SmoothPartitionOfUnity.sum_eq_one, ODE.contDiffOn_enat_Icc_of_hasDerivWithinAt, DifferentiableAt.differentiableAt_norm_of_smul, SchwartzMap.hasDerivAt, MeasureTheory.tendsto_eLpNorm_condExp, MeasureTheory.eLpNorm_one_condExp_le_eLpNorm, MeasureTheory.integral_of_ae_eq_zero_or_one, integral_log, signedDist_self, MeasureTheory.toReal_rnDeriv_map_ae_eq_trim, integral_sqrt_one_sub_sq, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos, circleAverage_log_norm_add_const_eq_posLog, Real.Gamma_eq_integral, signedDist_vsub_self, MeasureTheory.SignedMeasure.rnDeriv_smul, Affine.Simplex.exists_forall_signedInfDist_eq_iff_eq_incenter, signedDist_smul, MeromorphicOn.circleAverage_log_norm, ProbabilityTheory.charFun_inv_sqrt_mul_sum, ZLattice.volume_image_eq_volume_div_covolume, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, ContDiffOn.norm_sq, Real.map_linearMap_volume_pi_eq_smul_volume_pi, intervalIntegral.inv_mul_integral_comp_div_sub, Euclidean.closedBall_eq_preimage, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, Matrix.PosSemidef.inv_sqrt, intervalIntegral.differentiable_integral_of_continuous, integral_log_from_zero_of_pos, LipschitzWith.locallyIntegrable_lineDeriv, SmoothBumpCovering.embeddingPiTangent_injOn, ConvexOn.map_condExp_le, EulerSine.integral_cos_pow_eq, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, ConvexOn.average_mem_epigraph, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, MeasureTheory.integral_condExp_indicator, ContDiffWithinAt.abs, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, intervalIntegral.integral_comp_mul_deriv_of_deriv_nonpos, Orientation.abs_areaForm_of_orthogonal, ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess, LipschitzOnWith.ae_differentiableWithinAt_real, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, integral_sin, InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul, Function.hasTemperateGrowth_inner_left, exists_eq_const_mul_intervalIntegral_of_ae_nonneg, ContDiffAt.contDiffAt_norm_of_smul, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf, Real.le_integral_rpowIntegrand₀₁_one, ContinuousLinearMap.intervalIntegral_apply, analyticWithinAt_sigmoid, ProbabilityTheory.variance_le_expectation_sq, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral, analyticOn_sigmoid, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.integral_fin_nat_prod_eq_prod, MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.submartingale_of_expected_stoppedValue_mono, ContDiffBump.integral_le_measure_closedBall, mdifferentiableWithinAt_comp_projIcc_iff, Real.zero_at_infty_fourier, Orientation.inner_sq_add_areaForm_sq, intervalIntegral.integral_nonneg_of_ae_restrict, signedDist_smul_of_neg, nnnorm_fderiv_norm_rpow_le, Real.hasFPowerSeriesOnBall_linear_zero, differentiableAt_abs_pos, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero, Real.hasDerivAt_Gamma_one_half, ProbabilityTheory.isPosSemidef_covarianceBilinDual, fderiv_norm_smul, Diffeology.IsContDiffCompatible.isPlot_iff, MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, range_mfderiv_coe_sphere, ProbabilityTheory.strong_law_aux7, MeasureTheory.integrable_prod_iff', Affine.Simplex.sign_signedInfDist_touchpoint_empty, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, Real.one_add_rpow_hasFPowerSeriesAt_zero, integral_sin_pow_odd_mul_cos_pow, signedDist_vadd_right_swap, ProbabilityTheory.integral_condCDF, ValueDistribution.proximity_zero_of_complexValued, SchwartzMap.integralCLM_apply, EulerSine.tendsto_integral_cos_pow_mul_div, MeasureTheory.Submartingale.stoppedAbove, MeasureTheory.withDensityᵥ_toReal, ProbabilityTheory.Kernel.condExp_densityProcess, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.inner_basisFun_real, iccLeftChart_extend_zero, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, ProbabilityTheory.covarianceBilin_real, ProbabilityTheory.condVar_of_ae_eq_zero_or_one, bernoulliFun_eq_integral, ProbabilityTheory.moment_def, MeasureTheory.taylorWithinEval_charFun_two_zero, ProbabilityTheory.iIndepFun.integral_prod_eq_prod_integral, Euclidean.ball_eq_preimage, InformationTheory.rightDeriv_klFun_one, hasDerivAt_abs, NumberField.mixedEmbedding.stdBasis_apply_isReal, Function.RCLike.hasTemperateGrowth_ofReal, EuclideanSpace.volume_ball, ContDiffAt.norm, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, ProbabilityTheory.covarianceBilin_of_not_memLp, InformationTheory.rightDeriv_klFun, interior_range_modelWithCornersEuclideanHalfSpace, ExistsContDiffBumpBase.y_smooth, contDiff_inner, ProbabilityTheory.condVar_bot', Real.hasDerivAt_Gamma_one, IntervalIntegrable.intervalIntegrable_slope, ConvexOn.map_integral_le, Differentiable.dist, ProbabilityTheory.condVar_of_sigmaFinite, ContDiffAt.dist, innerSL_real_flip, tsum_sq_fourierCoeffOn, ProbabilityTheory.covarianceBilinDual_comm, ProbabilityTheory.iteratedDeriv_two_cgf, SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left, integral_exp_mul_Ioi, integral_sin_mul_cos_sq, ConcaveOn.condExp_map_le_of_finiteDimensional, SmoothPartitionOfUnity.exists_pos_of_mem, ProbabilityTheory.deriv_mgf_zero, intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le, Real.deriv_sigmoid, SchwartzMap.compCLM_apply, intervalIntegral.fderivWithin_integral_of_tendsto_ae, one_add_rpow_hasFPowerSeriesAt_zero, ProbabilityTheory.iCondIndepFun_iff, circleAverage_log_norm_sub_const_eq_posLog, Orientation.volumeForm_robust', exists_smooth_zero_one_of_isClosed, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, HasDerivAt.hasGradientAt', ContMDiff.inner_bundle, analyticAt_log, MeasureTheory.ae_mem_limsup_atTop_iff, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, signedDist_vadd_left, Diffeology.IsPlot.contDiff, ContDiffBump.convolution_eq_right, ExistsContDiffBumpBase.w_def, ProbabilityTheory.deriv_cgf, isBoundedBilinearMap_inner, intervalIntegral.integral_hasFDerivWithinAt, circleAverage_log_norm_factorizedRational, TopologicalGroup.IsSES.pushforward_mono, SmoothBumpCovering.embeddingPiTangent_injective, ContDiff.dist, ProbabilityTheory.covarianceBilin_apply, exists_contMDiff_support_eq_eq_one_iff, ProbabilityTheory.setIntegral_condVar, volume_regionBetween_eq_integral', MeasureTheory.ae_bdd_condExp_of_ae_bdd, hasDerivAt_norm_rpow, ContMDiffAt.inner_bundle, NumberField.mixedEmbedding.latticeBasis_apply, ConcaveOn.condExp_map_le_univ, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, signedDist_apply_linear_apply, SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul, MeasureTheory.charFun_map_mul_comp, InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul, AnalyticAt.harmonicAt_log_norm, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, ProbabilityTheory.covarianceBilin_map, AnalyticWithinAt.sigmoid, AffineSubspace.signedInfDist_singleton, Real.tsum_eq_tsum_fourier_of_rpow_decay, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, intervalIntegral.mul_integral_comp_mul_add, Bundle.ContinuousRiemannianMetric.pos, ProbabilityTheory.strong_law_aux4, SchwartzMap.derivCLM_apply, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop, Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, IsCoercive.continuousLinearEquivOfBilin_apply, intervalIntegral.integral_nonneg_of_ae, Orientation.volumeForm_zero_neg, SmoothPartitionOfUnity.contMDiff_finsum_smul, ContDiffBump.dist_normed_convolution_le, SmoothPartitionOfUnity.sum_finsupport, Orientation.areaForm_map, deriv_bernoulliFun, det_fderivPiPolarCoordSymm, ProbabilityTheory.condVar_bot_ae_eq, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, NumberField.mixedEmbedding.commMap_apply_of_isReal, Fourier.norm_fourierIntegral_le_integral_norm, intervalIntegral.integral_deriv_comp_mul_deriv, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos, ZSpan.fundamentalDomain_pi_basisFun, LipschitzWith.ae_differentiableAt_of_real, MeasureTheory.Measure.integrable_comp_iff, Bundle.RiemannianMetric.pos, IsOpen.exists_contDiff_support_eq, integral_zpow, exists_eq_interval_average_of_measure, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, Function.Complex.hasTemperateGrowth_ofReal, ConvexOn.map_average_le, ProbabilityTheory.analyticOnNhd_mgf, DifferentiableAt.abs, integral_one_div_one_add_sq, MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt, integral_one, circleAverage_log_norm_sub_const₂, Manifold.pathELength_eq_lintegral_mfderiv_Icc, MeasureTheory.hasFiniteIntegral_prod_iff, MeasureTheory.charFun_map_mul, Orientation.inner_rightAngleRotationAux₁_right, hasFDerivAt_pi_polarCoord_symm, ContDiffWithinAt.inner, NumberField.mixedEmbedding.latticeBasis_repr_apply, InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero, ProbabilityTheory.condVar_of_aestronglyMeasurable, DifferentiableWithinAt.norm_sq, Real.fourierIntegral_continuousLinearMap_apply', integral_sin_pow_succ_le, ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral, signedDist_right_lineMap, InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul, ProbabilityTheory.uncenteredCovarianceBilin_zero, integral_mulExpNegMulSq_comp_eq, Real.differentiable_fourierChar, hasFDerivAt_integral_of_dominated_of_fderiv_le, TopologicalAddGroup.IsSES.integral_inducedMeasure, ContDiff.abs, VectorFourier.fourierPowSMulRight_apply, OrthonormalBasis.norm_dual, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, DifferentiableOn.dist, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, NumberField.mixedEmbedding.normAtPlace_negAt, Chebyshev.integral_theta_div_log_sq_isBigO, AlternatingMap.measure_def, MeasureTheory.maximal_ineq, HasDerivAtFilter.hasGradientAtFilter', Real.tendsto_Icc_vitaliFamily_left, integral_le_sum_Ico_of_le, integral_gaussian, Orientation.areaForm_map_complex, intervalIntegral.integral_smul_const, intervalIntegral.mul_integral_comp_sub_mul, contMDiffOn_comp_projIcc_iff, intervalIntegral.abs_integral_eq_abs_integral_uIoc, NumberField.mixedEmbedding.finrank, integral_one_div, ProbabilityTheory.integral_id_gaussianReal, ProbabilityTheory.meas_ge_le_evariance_div_sq, SmoothBumpFunction.contMDiff, AnalyticAt.re_ofReal, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul', Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, Orientation.inner_rightAngleRotation_right, ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow, volume_euclideanSpace_eq_dirac, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, ConcaveOn.average_mem_hypograph, integral_sin_sq_mul_cos, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, intervalIntegral.norm_integral_le_integral_norm, Affine.Simplex.ExcenterExists.signedInfDist_excenter, Orientation.volumeForm_apply_le, BoxIntegral.Box.volume_apply, SmoothPartitionOfUnity.finite_tsupport, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, Complex.integral_rpow_mul_exp_neg_mul_rpow, TopologicalAddGroup.IsSES.pushforward_mono, NumberField.mixedEmbedding.negAt_apply_norm_isReal, Chebyshev.integral_theta_div_log_sq_isLittleO, deriv_inner_apply, EulerSine.integral_cos_pow_pos, MonotoneOn.integral_le_sum, MeasureTheory.pdf.IsUniform.integral_eq, ContDiff.norm, AntitoneOn.sum_le_integral, integral_pow_mul_le_of_le_of_pow_mul_le, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, hasDerivWithinAt_abs_neg, StieltjesFunction.ae_hasDerivAt, contDiffWithinAt_abs, hasSum_sq_fourierCoeff, ProbabilityTheory.strong_law_aux1, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot, Orientation.kahler_apply_apply, Orientation.inner_rightAngleRotationAux₁_left, exists_embedding_euclidean_of_compact, HasDerivAt.inner, Orientation.areaForm_apply_self, ProbabilityTheory.hasFiniteIntegral_compProd_iff, Real.differentiable_fourierChar_neg_bilinear_right, ProbabilityTheory.variance_linearMap_gaussianReal, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀, BumpCovering.coe_toSmoothPartitionOfUnity, AffineSubspace.signedInfDist_def, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, MeasureTheory.BoundedContinuousFunction.inner_toLp, MeasureTheory.taylorWithinEval_charFun_two_zero', MeasureTheory.integral_fintype_prod_volume_eq_prod, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, MeasureTheory.convolution_mono_right, signedDist_lineMap_right, ProbabilityTheory.integral_id_multivariateGaussian', MeasureTheory.Integrable.uniformIntegrable_condExp_filtration, Real.integral_rpow_mul_exp_neg_mul_Ioi, SchwartzMap.tsupport_derivCLM_subset, MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, SchwartzMap.integral_smul_laplacian_right_eq_left, SchwartzMap.le_seminorm', differentiable_norm_rpow, VectorFourier.fourierIntegral_probChar, Affine.Simplex.sign_signedInfDist_incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, ProbabilityTheory.evariance_eq_zero_iff, integral_inv_one_add_sq, VectorFourier.norm_fourierSMulRight_le, AlternatingMap.measure_parallelepiped, ProbabilityTheory.Kernel.setIntegral_density, Affine.Simplex.signedInfDist_affineCombination, tendsto_sum_mul_atTop_nhds_one_sub_integral, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, ProbabilityTheory.strong_law_aux2, intervalIntegral.mul_integral_comp_mul_right, Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero, signedDist_apply, ProbabilityTheory.iIndepFun.integral_fun_prod_eq_prod_integral, intervalIntegral.norm_integral_le_abs_integral_norm, UnitAddTorus.hasSum_sq_mFourierCoeff, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne, integral_sin_pow_odd, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, signedDist_eq_dist_iff_vsub_mem_span, volume_regionBetween_eq_integral, VectorFourier.norm_fourierPowSMulRight_le, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, Real.hasFDerivAt_fourierChar_neg_bilinear_right, intervalIntegral.inv_mul_integral_comp_div, ProbabilityTheory.strong_law_aux3, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral, VectorFourier.norm_fourierSMulRight, Function.Periodic.integral_le_sSup_add_zsmul_of_pos, differentiableOn_abs, norm_sub_le_integral_of_norm_deriv_le_of_le, ProbabilityTheory.hasDerivAt_mgf, InnerProductSpace.laplacian_eq_iteratedDeriv_real, taylor_mean_remainder_cauchy, MeasureTheory.Martingale.ae_eq_condExp_limitProcess, ContDiffAt.abs, intervalIntegral.integral_eq_zero_iff_of_nonneg_ae, ProbabilityTheory.strong_law_ae_real, Real.iteratedDeriv_fourierIntegral, ContDiffAt.inner, ExistsContDiffBumpBase.w_integral, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, ProbabilityTheory.deriv_cgf_zero, sum_mul_eq_sub_sub_integral_mul', intervalIntegral.integral_comp_mul_deriv', LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul, NumberField.mixedEmbedding.euclidean.finrank, ProbabilityTheory.multivariateGaussian_zero_one, DifferentiableAt.norm, Real.differentiable_fourierChar_neg_bilinear_left, fderiv_norm_smul_pos, integral_Ioi_inv_one_add_sq, Real.circleAverage_mono, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo, Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, range_modelWithCornersEuclideanHalfSpace, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, ProbabilityTheory.iIndepFun.integral_fun_prod_comp, integral_exp_neg_Ioi_zero, sum_mul_eq_sub_integral_mul, Orientation.areaForm_rightAngleRotation_right, MeasurableEquiv.gaussianReal_map_symm_apply, MDifferentiableAt.inner_bundle, AnalyticOnNhd.sigmoid, contDiff_norm_rpow, exists_contDiff_tsupport_subset, ProbabilityTheory.indepFun_iff_integral_comp_mul, Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, tsum_sq_fourierCoeff, BoundedContinuousFunction.charMonoidHom_apply, MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNorm, intervalIntegral.integral_pos, integral_sin_pow, ProbabilityTheory.iIndepFun.integral_prod_comp, AntitoneOn.integral_le_sum, integral_gaussian_Ioi, fderiv_norm_rpow, intervalIntegral_ofReal, Real.Icc_mem_vitaliFamily_at_right, ConcaveOn.le_map_set_average, Real.hasDerivAt_fourierIntegral, AnalyticOn.re_ofReal, MeasureTheory.integral_one_sub_of_ae_eq_zero_or_one, AffineSubspace.signedInfDist_apply_self, integral_sin_sq_mul_cos_sq, ProbabilityTheory.covarianceBilinDual_of_not_memLp, integral_mul_rpow_one_add_sq, EuclideanSpace.euclideanHausdorffMeasure_eq_volume, MeasureTheory.charFun_map_eq_charFunDual_smul, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico, ContMDiff.codRestrict_sphere, Real.tsum_eq_tsum_fourierIntegral, SchwartzMap.tsum_eq_tsum_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, MeasureTheory.condExpIndSMul_ae_eq_smul, Quaternion.linearIsometryEquivTuple_apply, MeasureTheory.intervalIntegrable_charFun, integral_Iic_inv_one_add_sq, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone, SmoothPartitionOfUnity.contMDiff_smul, ProbabilityTheory.condIndepFun_iff, BoxIntegral.norm_integral_le_of_norm_le, TemperedDistribution.derivCLM_apply_apply, integral_cos_sq, abs_signedDist_le_dist, NumberField.mixedEmbedding.disjoint_span_commMap_ker, mfderiv_subtype_coe_Icc_one, MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const, intervalIntegral.integral_hasFDerivAt, ValueDistribution.proximity_coe, MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto, intervalIntegral.fderiv_integral, ProbabilityTheory.gaussianReal_apply_eq_integral, ProbabilityTheory.IsGaussian.charFunDual_eq', MeasureTheory.integral_prod_smul, ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self, AffineSubspace.signedInfDist_apply_of_mem, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, Real.hasDerivAt_Gamma_nat, HasStrictFDerivAt.inner, TopologicalGroup.IsSES.integrate_mono, MeasureTheory.ContinuousMap.inner_toLp, ConvexOn.apply_rnDeriv_ae_le_integral, differentiableAt_abs, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul', intervalIntegral.norm_integral_le_abs_of_norm_le, ProbabilityTheory.analyticAt_iteratedDeriv_mgf, ProbabilityTheory.charFun_gaussianReal, exists_eq_interval_average, exists_smooth_zero_one_nhds_of_isClosed, DifferentiableOn.norm, integral_exp_Iic_zero, AnalyticOnNhd.log, ContDiffOn.norm, sum_mul_eq_sub_integral_mul₀, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, signedDist_apply_linear, Bundle.RiemannianMetric.continuousAt, parallelepiped_orthonormalBasis_one_dim, Real.fourierIntegral_deriv, integral_log_from_zero, MeasureTheory.integrable_mconv_iff, VectorFourier.norm_fourierIntegral_le_integral_norm, Manifold.exists_lt_of_riemannianEDist_lt, MeasureTheory.integral_abs_condExp_le, StrictConvexOn.ae_eq_const_or_map_average_lt, VectorFourier.hasFDerivAt_fourierChar_smul, OrthonormalBasis.measurePreserving_measurableEquiv, Real.fourierIntegral_real_eq, InformationTheory.not_differentiableAt_klFun_zero, MeasureTheory.measure_unitBall_eq_integral_div_gamma, Chebyshev.theta_eq_primeCounting_mul_log_sub_integral, integral_cos_sq_sub_sin_sq, ProbabilityTheory.variance_tilted_mul, MeasureTheory.le_integral_rnDeriv_of_ac, SmoothBumpCovering.embeddingPiTangent_coe, SchwartzMap.integral_smul_deriv_right_eq_neg_left, SmoothPartitionOfUnity.nonneg', taylor_mean_remainder_lagrange, ProbabilityTheory.covarianceBilinDual_of_not_memLp', Function.hasTemperateGrowth_one_add_norm_sq_rpow, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn, ContDiffWithinAt.norm, SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul, ProbabilityTheory.analyticOn_iteratedDeriv_mgf, MeasureTheory.Integrable.integral_norm_condKernel, intervalIntegral.inv_mul_integral_comp_div_add, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, Orientation.volumeForm_comp_linearIsometryEquiv, norm_fderiv_norm_id_rpow, NumberField.Units.basisOfIsMaxRank_fundSystem, Function.Periodic.tendsto_atTop_intervalIntegral_of_pos, NumberField.mixedEmbedding.fundamentalCone.linearIndependent_completeFamily, intervalIntegral.norm_integral_le_integral_norm_uIoc, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, Affine.Simplex.signedInfDist_apply_of_ne, sum_mul_eq_sub_sub_integral_mul, exists_contMDiffMap_one_nhds_of_subset_interior, signedDist_left_lineMap, DifferentiableWithinAt.inner, NumberField.mixedEmbedding.norm_negAt, SmoothPartitionOfUnity.sum_le_one, intervalIntegral.integral_comp_mul_deriv'', VectorFourier.fourierIntegral_fderiv, AnalyticWithinAt.log, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le, IccRightChart_extend_top, integral_one_div_of_neg, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg', ContDiffBump.convolution_tendsto_right_of_continuous, fderivInnerCLM_apply, intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero, ContMDiffWithinAt.inner_bundle, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le, boundary_Icc, MeasureTheory.tendsto_integral_meas_thickening_le, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fderiv_fourierChar_neg_bilinear_left_apply, Real.exists_measure_rpow_eq_integral, Real.fourierIntegral_continuousMultilinearMap_apply', ValueDistribution.proximity_top, ProbabilityTheory.integrable_comp_iff, MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul, integral_sin_pow_antitone, Matrix.PosDef.posDef_sqrt, integral_pow_abs_sub_uIoc, Real.circleAverage_nonneg_of_nonneg, EuclideanSpace.volume_closedBall, intervalIntegral.integral_nonneg_of_forall, InformationTheory.deriv_klFun, one_add_rpow_hasFPowerSeriesOnBall_zero, AnalyticOnNhd.im_ofReal, boundary_product, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, differentiable_sigmoid, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, DifferentiableAt.abs_of_pos, ProbabilityTheory.IsGaussian.eq_gaussianReal, Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, ProbabilityTheory.integral_tilted_mul_self, integrableOn_Ioi_deriv_norm_ofReal_cpow, AnalyticOn.log, DifferentiableAt.abs_of_neg, intervalIntegral.integral_mul_const, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv, ProbabilityTheory.cdf_gammaMeasure_eq_integral, MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul, MeasureTheory.toReal_rnDeriv_map, fourier_gaussian_pi, Function.Periodic.tendsto_atTop_intervalIntegral_of_pos', not_differentiableAt_abs_zero, MonotoneOn.ae_differentiableWithinAt, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, Orientation.areaForm_rightAngleRotation_left, Differentiable.norm, Real.deriv_fourier, contDiff_sigmoid, NumberField.mixedEmbedding.disjoint_negAt_plusPart, DifferentiableAt.dist, IccLeftChart_extend_bot_mem_frontier, fderiv_norm_sq_apply, LipschitzWith.ae_differentiableAt_real, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, MeasureTheory.integral_comp_mul_deriv_Ioi, Icc_isBoundaryPoint_top, integral_sin_pow_even, MeasureTheory.condExp_mul_of_stronglyMeasurable_left, MeasureTheory.Measure.euclideanHausdorffMeasure_def, fderiv_norm_sq, MeasureTheory.addEquivAddHaarChar_smul_integral_map, Orientation.inner_mul_inner_add_areaForm_mul_areaForm', ContDiffOn.dist, MDifferentiable.inner_bundle, fourierIntegral_gaussian_pi', hasDerivAt_abs_pos, LipschitzWith.integral_lineDeriv_mul_eq, MeasureTheory.condExpL2_indicator_nonneg, HasCompactSupport.hasFDerivAt_convolution_left, ProbabilityTheory.charFunDual_stdGaussian, instIsManifoldIcc, Bundle.ContinuousRiemannianMetric.isVonNBounded, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, Orientation.inner_mul_areaForm_sub, ProbabilityTheory.integral_preCDF_fst, fderiv_inner_apply, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, contDiffAt_abs, MeasureTheory.Integrable.uniformIntegrable_condExp, SmoothPartitionOfUnity.contMDiff_sum, contMDiffOn_projIcc, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, ContDiffBump.integral_pos, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, Metric.exists_contMDiffMap_forall_closedEBall_subset, BoxIntegral.unitPartition.tag_mem_smul_span, signedDist_vadd_vadd, parallelepiped_single, contMDiff_circleExp, SchwartzMap.tsum_eq_tsum_fourier, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral, hasFDerivAt_integral_of_dominated_loc_of_lip, intervalIntegral.norm_integral_le_of_norm_le, MeasureTheory.taylorWithinEval_charFun_zero, GaussianFourier.integral_rexp_neg_mul_sq_norm, Real.tendsto_Icc_vitaliFamily_right, BoundedContinuousFunction.char_apply, intervalIntegral.differentiableOn_integral_of_continuous, differentiable_circleMap, AnalyticAt.im_ofReal, Function.Periodic.tendsto_atBot_intervalIntegral_of_pos, intervalIntegral.integral_nonneg, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf, Orientation.abs_volumeForm_apply_le, intervalIntegral.mul_integral_comp_mul_left, Affine.Simplex.signedInfDist_incenter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_apply 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	—
inner_apply' 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	mul_comm

(root)

Definitions

Name	Category	Theorems
bilinFormOfRealInner 📖	CompOp	—
innerₗ 📖	CompOp	13 math math: isNonneg_inner, MeasureTheory.charFun_eq_fourierIntegral', MeasureTheory.charFun_eq_fourierIntegral, isSymm_inner, innerₗ_apply, orthogonalBilin_innerₗ, InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace, innerₗ_apply_apply, bilinFormOfRealInner_orthogonal, flip_innerₗ, ProperCone.innerDual_toSubmodule, signedDist_apply_linear, isPosSemidef_inner
innerₛₗ 📖	CompOp	16 math math: LinearMap.adjoint_innerₛₗ_apply, innerₛₗ_apply_apply, LinearMap.toMatrix_innerₛₗ_apply, ContinuousLinearMap.toLinearMap_innerSL_apply, LinearMap.adjoint_toSpanSingleton, Orientation.inner_mul_areaForm_sub', toMatrix_innerSL_apply, InnerProductSpace.toLinearMap_rankOne, LinearMap.isSymmetric_iff_sesqForm, innerₛₗ_apply, ContinuousLinearMap.isAdjointPair_inner, innerₛₗ_apply_coe, LinearPMap.mem_adjoint_domain_iff, coe_innerₛₗ_apply, LinearMap.isAdjointPair_inner, Orientation.inner_mul_inner_add_areaForm_mul_areaForm'
instInnerProductSpaceRealComplex 📖	CompOp	350 math math: NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, TemperedDistribution.lineDerivOpCLM_eq, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, MeasureTheory.Lp.toTemperedDistributionCLM_apply, Orientation.kahler_map_complex, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, EulerSine.integral_cos_mul_cos_pow, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, Distribution.dsupport_delta, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, MeasureTheory.contDiff_charFun', Complex.kahler, Complex.areaForm, finrank_real_complex_fact', MeasureTheory.charFunDual_apply, Complex.norm_sub_mem_Icc_angle, Complex.integral_comp_pi_polarCoord_symm, PeriodPair.basis_one, Orientation.kahler_comp_rightAngleRotation', circleIntegral_def_Icc, circleIntegrable_iff, Real.fderiv_fourierChar_neg_bilinear_right_apply, MeasureTheory.iteratedDeriv_charFun_zero, GaussianFourier.integral_cexp_neg_mul_sq_norm, Complex.angle_exp_one, TemperedDistribution.fourierMultiplierCLM_smul, Complex.angle_div_right_eq_angle_mul_left, Complex.betaIntegral_scaled, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, TemperedDistribution.lineDerivOp_fourier_eq, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, Complex.oangle, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, intervalIntegral.integral_ofReal, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, Distribution.IsVanishingOn.smulLeftCLM, Complex.angle_mul_left, analyticOnNhd_circleMap, NumberField.mixedEmbedding.commMap_apply_of_isComplex, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, Complex.toBasis_orthonormalBasisOneI, HarmonicAt.analyticAt_complex_partial, NumberField.mixedEmbedding.convexBodyLT_volume, Complex.integral_rpow_mul_exp_neg_rpow, SchwartzMap.integral_fourierInv_smul_eq, Complex.volume_sum_rpow_le, SchwartzMap.inner_toL2_toL2_eq, Complex.mul_angle_le_norm_sub, Complex.coe_orthonormalBasisOneI, NumberField.mixedEmbedding.negAt_apply_snd, MeasureTheory.charFun_apply, TemperedDistribution.smulLeftCLM_neg, AnalyticAt.harmonicAt_im, Function.HasTemperateGrowth.toTemperedDistribution_apply, NumberField.mixedEmbedding.negAt_preimage, Complex.hasDerivAt_GammaIntegral, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, MeasureTheory.charFun_apply_real, EulerSine.integral_cos_mul_cos_pow_aux, TemperedDistribution.instLineDerivLeftSMulReal, MeasureTheory.iteratedFDeriv_charFun, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, TemperedDistribution.fourierInv_lineDerivOp_eq, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, Orientation.kahler_eq_zero_iff, Complex.integral_comp_polarCoord_symm, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, integral_exp_mul_complex_Ioi, setIntegral_Ioi_zero_cpow, TemperedDistribution.instFourierAdd, Complex.sameRay_of_arg_eq, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, Orientation.kahler_swap, Orientation.rotation_map_complex, TemperedDistribution.instFourierSMul, contDiff_circleMap, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, Orientation.kahler_comp_rightAngleRotation, TemperedDistribution.delta_apply, integral_exp_mul_complex, TemperedDistribution.instContinuousFourier, Complex.integral_exp_neg_rpow, PeriodPair.basis_zero, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Complex.orthonormalBasisOneI_repr_apply, SchwartzMap.delta_apply, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, integral_cpow, ProbabilityTheory.iteratedDeriv_complexMGF, LSeries_eq_mul_integral_of_nonneg, Complex.angle_mul_right, HarmonicAt.differentiableAt_complex_partial, EulerSine.sin_pi_mul_eq, integral_mul_cexp_neg_mul_sq, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, integral_exp_mul_I_eq_sinc, TemperedDistribution.fourierMultiplierCLM_const, NumberField.mixedEmbedding.mem_span_latticeBasis, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, Orientation.kahler_neg_orientation, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, SchwartzMap.toTemperedDistributionCLM_apply_apply, integrableOn_Ioi_deriv_ofReal_cpow, integral_exp_mul_I_eq_sin, Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable, TemperedDistribution.smulLeftCLM_sub, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, Complex.angle_eq_abs_arg, NumberField.mixedEmbedding.negAt_apply_isComplex, ProbabilityTheory.isGaussian_iff_charFun_eq, Polynomial.rootSet_derivative_subset_convexHull_rootSet, has_antideriv_at_fourier_neg, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, UpperHalfPlane.smulFDeriv_J_mul, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, inner_map_complex, Polynomial.eq_centerMass_of_eval_derivative_eq_zero, hasDerivAt_fourier_neg, AnalyticAt.harmonicAt_conj, MeasureTheory.integral_charFun_Icc, instFiniteDimensionalRealComplex, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, ProbabilityTheory.hasDerivAt_complexMGF, ProbabilityTheory.IsGaussian.charFunDual_eq, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, Complex.integral_exp_neg_mul_rpow, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, TemperedDistribution.instLineDerivSMulReal, MeasureTheory.Measure.toTemperedDistribution_apply, ContDiffAt.harmonicAt, Complex.norm_sub_le_angle, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, TemperedDistribution.fourier_lineDerivOp_eq, Complex.volume_sum_rpow_lt, HarmonicAt.analyticAt, Complex.lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, NumberField.mixedEmbedding.span_latticeBasis, integral_cexp_quadratic, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, Complex.orthonormalBasisOneI_repr_symm_apply, hasDerivAt_circleMap, TemperedDistribution.laplacian_eq_sum, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, TemperedDistribution.instContinuousLineDeriv, hasDerivAt_fourier, Complex.volume_preserving_equiv_real_prod, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, Complex.angle_div_left_eq_angle_mul_right, Distribution.IsVanishingOn.iteratedLineDerivOp, LSeries_eq_mul_integral, deriv_circleMap, NumberField.mixedEmbedding.covolume_integerLattice, Orientation.kahler_apply_self, Orientation.kahler_rotation_left', Distribution.dsupport_smulLeftCLM_subset, Complex.angle_le_mul_norm_sub, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, TemperedDistribution.smulLeftCLM_add, Orientation.normSq_kahler, Complex.volume_closedBall, NumberField.mixedEmbedding.negAt_symm, MeasureTheory.iteratedDeriv_charFun, Complex.inner, AnalyticAt.harmonicAt_re, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, MeasureTheory.measureReal_abs_gt_le_integral_charFun, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, NumberField.mixedEmbedding.volume_negAt_plusPart, NumberField.mixedEmbedding.convexBodyLT'_volume, TemperedDistribution.fourierTransform_apply, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, Orientation.kahler_rightAngleRotation_left, Orientation.kahler_comp_linearIsometryEquiv, Real.hasDerivAt_fourierChar, Orientation.kahler_rotation_left, LindemannWeierstrass.integral_exp_mul_eval, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, SchwartzMap.integral_fourier_mul_eq, Complex.volume_preserving_equiv_pi, EulerSine.tendsto_integral_cos_pow_mul_div, NumberField.mixedEmbedding.volume_eq_zero, MeasureTheory.taylorWithinEval_charFun_two_zero, NumberField.mixedEmbedding.stdBasis_apply_isReal, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, EulerSine.antideriv_cos_comp_const_mul, Orientation.kahler_mul, GaussianFourier.integral_cexp_neg_mul_sum_add, ProbabilityTheory.isGaussian_iff_charFunDual_eq, fourierIntegral_gaussian, TemperedDistribution.fourierMultiplierCLM_apply_apply, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, EulerSine.antideriv_sin_comp_const_mul, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun, TemperedDistribution.instFourierInvSMul, integral_gaussian_sq_complex, Distribution.dsupport_iteratedLineDerivOp_subset, Orientation.kahler_map, TemperedDistribution.instFourierInvAdd, UnitAddTorus.hasSum_prod_mFourierCoeff, NumberField.mixedEmbedding.latticeBasis_apply, TemperedDistribution.fourierInv_apply, AnalyticAt.harmonicAt_log_norm, MeasureTheory.contDiff_charFun, MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.instLineDerivAdd, Complex.GammaSeq_eq_approx_Gamma_integral, NumberField.mixedEmbedding.commMap_apply_of_isReal, Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real, TemperedDistribution.instLineDerivSMulComplex, Function.Complex.hasTemperateGrowth_ofReal, Complex.log_eq_integral, NumberField.mixedEmbedding.latticeBasis_repr_apply, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, Real.differentiable_fourierChar, NumberField.mixedEmbedding.normAtPlace_negAt, Distribution.dsupport_lineDerivOp_subset, Complex.isometryOfOrthonormal_apply, Complex.sameRay_iff, TemperedDistribution.fourierMultiplierCLM_sum, Orientation.areaForm_map_complex, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, NumberField.mixedEmbedding.finrank, SchwartzMap.integral_fourier_smul_eq, GaussianFourier.integral_cexp_neg_sum_mul_add, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Complex.sameRay_iff_arg_div_eq_zero, Complex.integral_rpow_mul_exp_neg_mul_rpow, NumberField.mixedEmbedding.negAt_apply_norm_isReal, Complex.angle_one_left, Complex.volume_ball, Real.deriv_fourierChar, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, Orientation.kahler_apply_apply, Complex.angle_one_right, Real.differentiable_fourierChar_neg_bilinear_right, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, MeasureTheory.taylorWithinEval_charFun_two_zero', TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, TemperedDistribution.isVanishingOn_delta, Orientation.kahler_rotation_right, integral_Ioi_cpow_of_lt, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, TemperedDistribution.lineDerivOp_apply_apply, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, TemperedDistribution.lineDerivOp_fourierInv_eq, Complex.lintegral_comp_pi_polarCoord_symm, AnalyticAt.harmonicAt, ProbabilityTheory.IsGaussian.charFun_eq, integral_gaussian_complex, SchwartzMap.integral_inner_fourier_fourier, integral_exp_mul_complex_Iic, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, TemperedDistribution.smulLeftCLM_sum, NumberField.mixedEmbedding.euclidean.finrank, Real.differentiable_fourierChar_neg_bilinear_left, Complex.volume_sum_rpow_lt_one, TemperedDistribution.instContinuousFourierInv, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, TemperedDistribution.fourier_apply, Complex.integral_boundary_rect_of_differentiableOn_real, SchwartzMap.coe_apply, integral_mul_cpow_one_add_sq, Orientation.oangle_map_complex, CircleIntegrable.out, Complex.rightAngleRotation, TemperedDistribution.smulLeftCLM_smul, deriv_circleMap_eq_zero_iff, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, PeriodPair.indep, SchwartzMap.tsum_eq_tsum_fourierIntegral, Orientation.kahler_rightAngleRotation_right, MeasureTheory.charFun_eq_integral_innerProbChar, TemperedDistribution.derivCLM_apply_apply, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, Orientation.norm_kahler, NumberField.mixedEmbedding.disjoint_span_commMap_ker, Complex.isometryOfOrthonormal_symm_apply, NumberField.mixedEmbedding.convexBodySum_volume, Complex.map_isometryOfOrthonormal, TemperedDistribution.fourierTransformInv_apply, PeriodPair.lattice_eq_span_range_basis, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, Complex.log_inv_eq_integral, Complex.integral_cpow_mul_exp_neg_mul_Ioi, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, integral_cos_mul_complex, NumberField.mixedEmbedding.norm_negAt, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, Complex.approx_Gamma_integral_tendsto_Gamma_integral, Real.fderiv_fourierChar_neg_bilinear_left_apply, UpperHalfPlane.hasStrictFDerivAt_smul, UpperHalfPlane.det_smulFDeriv, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, Distribution.IsVanishingOn.lineDerivOp, LSeries_eq_mul_integral', TemperedDistribution.laplacianCLM_apply, continuousAt_gaussian_integral, Orientation.rightAngleRotation_map_complex, NumberField.mixedEmbedding.disjoint_negAt_plusPart, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, EulerSine.integral_cos_mul_cos_pow_even, MeasureTheory.Lp.toTemperedDistribution_smul_eq, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, MeasureTheory.charFun_eq_integral_probChar, integral_gaussian_complex_Ioi, TemperedDistribution.smulLeftCLM_apply_apply, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, Complex.rotation, SchwartzMap.tsum_eq_tsum_fourier, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, MeasureTheory.taylorWithinEval_charFun_zero, PeriodPair.instIsZLatticeRealComplexLattice, differentiable_circleMap, Complex.angle_exp_exp, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm
sesqFormOfInner 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_real_inner_div_norm_mul_norm_eq_one_iff 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instOne SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace	—	norm_inner_div_norm_mul_norm_eq_one_iff
abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid abs Real.lattice Real.instAddGroup Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instOne	—	norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
abs_real_inner_div_norm_mul_norm_le_one 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instMul Norm.norm SeminormedAddCommGroup.toNorm Real.instOne	—	abs_div Real.instIsStrictOrderedRing abs_mul Real.instIsOrderedRing abs_norm div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instZeroLEOneClass abs_real_inner_le_norm mul_nonneg IsOrderedRing.toPosMulMono norm_nonneg
abs_real_inner_le_norm 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	LE.le.trans Eq.ge Real.norm_eq_abs norm_inner_le_norm
coe_innerₛₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike starRingEnd Semifield.toCommSemiring RCLike.toStarRing LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id innerₛₗ Inner.inner InnerProductSpace.toInner	—	Algebra.to_smulCommClass
dist_div_norm_sq_smul 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Monoid.toPow DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedAddCommGroup.toNorm Real.instMul	—	dist_eq_norm Real.sqrt_sq norm_nonneg Nat.instAtLeastTwoHAddOfNat sq norm_sub_mul_self_real norm_smul NormedSpace.toNormSMulClass Real.norm_of_nonneg mul_self_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inner_smul_right real_inner_smul_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt norm_pos_iff Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Real.sqrt_mul Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing even_two_mul Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_pos
eq_of_norm_le_re_inner_eq_norm_sq 📖	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Monoid.toPow Real.instMonoid	—	—	pow_le_pow_left₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono norm_nonneg inner_conj_symm RCLike.conj_re inner_sub_right inner_sub_left inner_self_eq_norm_sq_to_K map_sub AddMonoidHom.instAddMonoidHomClass RCLike.re_ofReal_pow sub_self sub_zero AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add sub_eq_zero re_inner_self_nonpos
ext_iff_inner_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup	—	ext_inner_left
ext_iff_inner_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup	—	ext_inner_right
ext_inner_left 📖	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup	—	—	sub_eq_zero inner_self_eq_zero inner_sub_right
ext_inner_right 📖	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup	—	—	sub_eq_zero inner_self_eq_zero inner_sub_left
flip_innerₗ 📖	mathematical	—	LinearMap.flip Real Real.semiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id RingHom.id Semiring.toNonAssocSemiring innerₗ	—	LinearMap.ext SMulCommClass.symm Algebra.to_smulCommClass real_inner_comm
im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im Inner.inner InnerProductSpace.toInner DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SMulZeroClass.toSMul AddZero.toZero SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.I AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat norm_sub_mul_self inner_smul_right RCLike.I_mul_re norm_add_mul_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
inner_add_add_self 📖	mathematical	—	Inner.inner InnerProductSpace.toInner AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_add_right inner_add_left Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
inner_add_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	InnerProductSpace.add_left
inner_add_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_conj_symm inner_add_left map_add SemilinearMapClass.toAddHomClass RCLike.charZero_rclike RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass
inner_conj_symm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.instFunLike starRingEnd RCLike.toStarRing Inner.inner InnerProductSpace.toInner	—	InnerProductSpace.conj_inner_symm
inner_eq_neg_one_iff_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	neg_eq_iff_eq_neg inner_neg_right inner_eq_one_iff_of_norm_eq_one norm_neg
inner_eq_norm_mul_iff 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	—	eq_or_ne inner_zero_left norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul smul_zero zero_smul inner_eq_norm_mul_iff_div div_eq_inv_mul SemigroupAction.mul_smul inv_smul_eq_iff₀ RCLike.ofReal_eq_zero norm_eq_zero
inner_eq_norm_mul_iff_div 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	List.TFAE.out norm_inner_eq_norm_tfae norm_mul NormedDivisionRing.toNormMulClass norm_algebraMap' NormedDivisionRing.to_normOneClass norm_norm inner_self_eq_norm_sq_to_K norm_smul NormedSpace.toNormSMulClass norm_div norm_pow map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_div₀ RingHomClass.toMonoidWithZeroHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass RCLike.ofReal_eq_zero norm_ne_zero_iff inner_smul_right Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf
inner_eq_norm_mul_iff_real 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace	—	inner_eq_norm_mul_iff
inner_eq_norm_sq_left_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instZero	—	inner_eq_ofReal_norm_sq_left_iff
inner_eq_norm_sq_right_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instZero	—	inner_eq_ofReal_norm_sq_right_iff
inner_eq_ofReal_norm_sq_left_iff 📖	mathematical	—	Inner.inner InnerProductSpace.toInner Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	inner_sub_right sub_eq_zero inner_self_eq_norm_sq_to_K
inner_eq_ofReal_norm_sq_right_iff 📖	mathematical	—	Inner.inner InnerProductSpace.toInner Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	inner_sub_left sub_eq_zero inner_self_eq_norm_sq_to_K
inner_eq_one_iff_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one one_smul inner_eq_norm_mul_iff
inner_eq_one_iff_of_norm_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_eq_one_iff_of_norm_eq_one
inner_eq_sum_norm_sq_div_four 📖	mathematical	—	Inner.inner InnerProductSpace.toInner DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RCLike.ofReal Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.I instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.re_add_im re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four RCLike.ofReal_div algebraMap.coe_sub algebraMap.coe_mul RCLike.ofReal_ofNat sq
inner_eq_zero_of_left 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm Real Real.instZero	Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	norm_eq_zero le_antisymm LE.le.trans norm_inner_le_norm MulZeroClass.zero_mul instReflLe norm_nonneg
inner_eq_zero_of_right 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm Real Real.instZero	Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_eq_zero_symm inner_eq_zero_of_left
inner_eq_zero_symm 📖	mathematical	—	Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_conj_symm star_eq_zero
inner_im_symm 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im Inner.inner InnerProductSpace.toInner Real.instNeg	—	inner_conj_symm RCLike.conj_im
inner_lt_norm_mul_iff_real 📖	mathematical	—	Real Real.instLT Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	ne_of_lt lt_of_le_of_ne real_inner_le_norm inner_eq_norm_mul_iff_real
inner_lt_one_iff_real_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Real Real.instLT Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instOne	—	mul_one one_smul inner_lt_norm_mul_iff_real
inner_lt_one_iff_real_of_norm_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Real Real.instLT Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instOne	—	inner_lt_one_iff_real_of_norm_eq_one
inner_mul_inner_self_le 📖	mathematical	—	Real Real.instLE Real.instMul Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re	—	InnerProductSpace.Core.inner_mul_inner_self_le
inner_mul_symm_re_eq_norm 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Inner.inner InnerProductSpace.toInner Norm.norm NormedField.toNorm	—	inner_conj_symm mul_comm RCLike.re_eq_norm_of_mul_conj
inner_neg_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	neg_one_smul inner_smul_left map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass RCLike.charZero_rclike SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass neg_mul one_mul
inner_neg_neg 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	inner_neg_right inner_neg_left neg_neg
inner_neg_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_conj_symm inner_neg_left map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass RCLike.charZero_rclike SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass
inner_re_symm 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	inner_conj_symm RCLike.conj_re
inner_re_zero_left 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instZero	—	inner_zero_left map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
inner_re_zero_right 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instZero	—	inner_zero_right map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
inner_self_conj 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.instFunLike starRingEnd RCLike.toStarRing Inner.inner InnerProductSpace.toInner	—	inner_conj_symm
inner_self_eq_norm_mul_norm 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	norm_eq_sqrt_re_inner Real.sqrt_mul inner_self_nonneg Real.sqrt_mul_self
inner_self_eq_norm_sq 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm	—	pow_two inner_self_eq_norm_mul_norm
inner_self_eq_norm_sq_to_K 📖	mathematical	—	Inner.inner InnerProductSpace.toInner Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal Norm.norm SeminormedAddCommGroup.toNorm	—	inner_self_ofReal_re InnerProductSpace.norm_sq_eq_re_inner RCLike.ofReal_pow
inner_self_eq_one_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_eq_one_iff_of_norm_eq_one
inner_self_eq_one_of_norm_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_self_eq_one_of_norm_eq_one
inner_self_eq_zero 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	inner_self_eq_norm_sq_to_K sq_eq_zero_iff isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.ofReal_eq_zero norm_eq_zero
inner_self_im 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im Inner.inner InnerProductSpace.toInner Real.instZero	—	Nat.instAtLeastTwoHAddOfNat RCLike.im_eq_conj_sub inner_conj_symm sub_self MulZeroClass.mul_zero zero_div map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
inner_self_ne_zero 📖	—	—	—	—	Iff.not inner_self_eq_zero
inner_self_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	PreInnerProductSpace.Core.re_inner_nonneg
inner_self_ofReal_norm 📖	mathematical	—	RCLike.ofReal Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner	—	inner_self_re_eq_norm inner_self_ofReal_re
inner_self_ofReal_re 📖	mathematical	—	RCLike.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	List.TFAE.out RCLike.is_real_TFAE inner_self_im
inner_self_re_eq_norm 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner Norm.norm NormedField.toNorm	—	inner_self_ofReal_re RCLike.norm_of_nonneg inner_self_nonneg
inner_smul_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike starRingEnd RCLike.toStarRing	—	inner_smul_left_eq_star_smul IsScalarTower.left StarMul.toStarModule
inner_smul_left_eq_smul 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_smul_left_eq_star_smul starRingEnd_apply TrivialStar.star_trivial
inner_smul_left_eq_star_smul 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike starRingEnd	—	algebraMap_smul InnerProductSpace.smul_left starRingEnd_apply algebraMap_star_comm smul_eq_mul IsScalarTower.right
inner_smul_real_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.ofReal Real Algebra.toSMul Semifield.toCommSemiring Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra	—	inner_smul_left RCLike.conj_ofReal Algebra.smul_def
inner_smul_real_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.ofReal Real Algebra.toSMul Semifield.toCommSemiring Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra	—	inner_smul_right Algebra.smul_def
inner_smul_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	inner_smul_right_eq_smul IsScalarTower.left StarMul.toStarModule
inner_smul_right_eq_smul 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_conj_symm inner_smul_left_eq_star_smul starRingEnd_apply StarModule.star_smul star_star
inner_sub_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	sub_eq_add_neg inner_add_left inner_neg_left
inner_sub_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	sub_eq_add_neg inner_add_right inner_neg_right
inner_sub_sub_self 📖	mathematical	—	Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing	—	inner_sub_right inner_sub_left Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
inner_sum 📖	mathematical	—	Inner.inner InnerProductSpace.toInner Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Algebra.to_smulCommClass
inner_sum_smul_sum_smul_of_sum_eq_zero 📖	mathematical	Finset.sum Real Real.instAddCommMonoid Real.instZero	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.instAddCommMonoid Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sum_inner Finset.sum_congr inner_sum real_inner_smul_left real_inner_smul_right real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two add_div mul_sub_left_distrib left_distrib Distrib.leftDistribClass Finset.sum_sub_distrib Finset.sum_add_distrib MulZeroClass.zero_mul MulZeroClass.mul_zero Finset.sum_const_zero zero_add zero_sub Finset.mul_sum neg_div Finset.sum_div mul_div_assoc mul_assoc
inner_zero_left 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	zero_smul inner_smul_left map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul
inner_zero_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_conj_symm inner_zero_left map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
innerₗ_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id innerₗ Inner.inner InnerProductSpace.toInner	—	Algebra.to_smulCommClass
innerₛₗ_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike starRingEnd Semifield.toCommSemiring RCLike.toStarRing LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id innerₛₗ Inner.inner InnerProductSpace.toInner	—	Algebra.to_smulCommClass
instSymmEqInnerOfNat 📖	mathematical	—	Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	inner_eq_zero_symm
isNonneg_inner 📖	mathematical	—	LinearMap.IsNonneg Real Real.instCommSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike RingHom.id Semiring.toNonAssocSemiring Real.semiring Real.instLE innerₗ	—	Algebra.to_smulCommClass inner_self_eq_norm_sq_to_K IsOrderedRing.toPosMulMono Real.instIsOrderedRing
isPosSemidef_inner 📖	mathematical	—	LinearMap.IsPosSemidef Real Real.instCommSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike RingHom.id Semiring.toNonAssocSemiring Real.semiring Real.instLE innerₗ	—	isSymm_inner isNonneg_inner
isSymm_inner 📖	mathematical	—	LinearMap.IsSymm Real Real.instCommSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike RingHom.id Semiring.toNonAssocSemiring Real.semiring innerₗ	—	Algebra.to_smulCommClass real_inner_comm
linearIndependent_of_ne_zero_of_inner_eq_zero 📖	mathematical	Pairwise Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	—	linearIndependent_iff' inner_sum inner_smul_right Finset.sum_eq_single MulZeroClass.mul_zero inner_self_eq_norm_sq_to_K inner_zero_right NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass isReduced_of_noZeroDivisors Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsSimpleRing.instNontrivial DivisionRing.isSimpleRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
neg_one_le_real_inner_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Real Real.instLE Real.instNeg Real.instOne Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	mul_one neg_le_of_abs_le Real.instIsOrderedAddMonoid abs_real_inner_le_norm
nnnorm_inner_le_nnnorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	norm_inner_le_norm
norm_add_eq_iff_real 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	pow_left_inj₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg Left.add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid two_ne_zero Nat.instAtLeastTwoHAddOfNat norm_add_sq add_pow_two instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le RCLike.re_to_real mul_assoc mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain CharZero.NeZero.two RCLike.charZero_rclike inner_eq_norm_mul_iff_real
norm_add_eq_sqrt_iff_real_inner_eq_zero 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.sqrt Real Real.instAdd Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instZero	—	norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero Real.sqrt_eq_iff_mul_self_eq add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg
norm_add_mul_self 📖	mathematical	—	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	Nat.instAtLeastTwoHAddOfNat sq norm_add_sq
norm_add_mul_self_real 📖	mathematical	—	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner Real.instRCLike	—	Nat.instAtLeastTwoHAddOfNat norm_add_mul_self
norm_add_pow_two 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	norm_add_sq
norm_add_pow_two_real 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner Real.instRCLike	—	norm_add_sq_real
norm_add_sq 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	Nat.instAtLeastTwoHAddOfNat sq inner_self_eq_norm_mul_norm inner_add_add_self two_mul add_assoc map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inner_conj_symm RCLike.conj_re
norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero 📖	mathematical	—	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instZero	—	Nat.instAtLeastTwoHAddOfNat norm_add_mul_self add_right_cancel_iff instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_eq_left mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero 📖	mathematical	Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat norm_add_mul_self add_right_cancel_iff instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_eq_left mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.zero_re
norm_add_sq_eq_norm_sq_add_norm_sq_real 📖	mathematical	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Real.instZero	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd	—	norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero
norm_add_sq_real 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner Real.instRCLike	—	Nat.instAtLeastTwoHAddOfNat norm_add_sq
norm_eq_sqrt_re_inner 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm Real.sqrt DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	Real.sqrt_sq norm_nonneg InnerProductSpace.norm_sq_eq_re_inner
norm_eq_sqrt_real_inner 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm Real.sqrt Inner.inner Real InnerProductSpace.toInner Real.instRCLike	—	norm_eq_sqrt_re_inner
norm_inner_div_norm_mul_norm_eq_one_iff 📖	mathematical	—	Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing RCLike.ofReal NormedAddCommGroup.toNorm Real Real.instOne SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	—	inner_zero_left norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul div_zero NeZero.charZero_one RCLike.charZero_rclike inner_zero_right MulZeroClass.mul_zero norm_inner_eq_norm_iff eq_of_div_eq_one norm_div norm_mul NormedDivisionRing.toNormMulClass norm_algebraMap' NormedDivisionRing.to_normOneClass norm_norm RCLike.norm_ofReal abs_norm norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Real.instMul NormedAddCommGroup.toNorm Real.instOne	—	inner_smul_right norm_mul NormedDivisionRing.toNormMulClass inner_self_re_eq_norm inner_self_eq_norm_mul_norm norm_smul NormedSpace.toNormSMulClass mul_assoc div_div mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass mul_comm div_self
norm_inner_eq_norm_iff 📖	mathematical	—	Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul NormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	—	List.TFAE.out norm_inner_eq_norm_tfae smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero
norm_inner_eq_norm_tfae 📖	mathematical	—	List.TFAE Real Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul NormedAddCommGroup.toNorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Submodule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet	—	pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass norm_ne_zero_iff div_eq_inv_mul SemigroupAction.mul_smul sub_eq_zero InnerProductSpace.Core.normSq_eq_zero InnerProductSpace.Core.cauchy_schwarz_aux InnerProductSpace.norm_sq_eq_re_inner mul_sub mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain mul_pow sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg mul_nonneg IsOrderedRing.toPosMulMono le_of_lt norm_pos_iff inv_smul_smul₀ inner_self_ne_zero inner_zero_left norm_zero MulZeroClass.zero_mul inner_smul_right inner_self_eq_norm_sq_to_K sq norm_mul norm_algebraMap' NormedDivisionRing.to_normOneClass norm_norm norm_smul NormedSpace.toNormSMulClass mul_left_comm List.tfae_of_cycle
norm_inner_le_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner Real.instMul SeminormedAddCommGroup.toNorm	—	norm_eq_sqrt_re_inner InnerProductSpace.Core.norm_inner_le_norm
norm_inner_symm 📖	mathematical	—	Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner	—	inner_conj_symm RCLike.norm_conj
norm_sub_eq_norm_add 📖	mathematical	Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing norm_nonneg inner_self_eq_norm_mul_norm inner_sub_right inner_sub_left sub_zero map_sub AddMonoidHom.instAddMonoidHomClass inner_re_symm RCLike.zero_re zero_sub sub_neg_eq_add inner_add_right map_add AddMonoidHomClass.toAddHomClass add_zero zero_add
norm_sub_eq_sqrt_iff_real_inner_eq_zero 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.sqrt Real Real.instAdd Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instZero	—	norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero Real.sqrt_eq_iff_mul_self_eq add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg
norm_sub_mul_self 📖	mathematical	—	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	Nat.instAtLeastTwoHAddOfNat sq norm_sub_sq
norm_sub_mul_self_real 📖	mathematical	—	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner Real.instRCLike	—	Nat.instAtLeastTwoHAddOfNat norm_sub_mul_self
norm_sub_pow_two 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	norm_sub_sq
norm_sub_pow_two_real 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner Real.instRCLike	—	norm_sub_sq_real
norm_sub_sq 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg norm_add_sq norm_neg inner_neg_right map_neg AddMonoidHom.instAddMonoidHomClass mul_neg
norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero 📖	mathematical	—	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instZero	—	Nat.instAtLeastTwoHAddOfNat norm_sub_mul_self add_right_cancel_iff instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_eq_add_neg add_eq_left neg_eq_zero mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike
norm_sub_sq_eq_norm_sq_add_norm_sq_real 📖	mathematical	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Real.instZero	Real Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd	—	norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero
norm_sub_sq_real 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner Real.instRCLike	—	norm_sub_sq
parallelogram_law 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat inner_add_add_self inner_sub_sub_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
parallelogram_law_with_nnnorm 📖	mathematical	—	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sq parallelogram_law_with_nnnorm_mul
parallelogram_law_with_nnnorm_mul 📖	mathematical	—	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Distrib.toMul NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat parallelogram_law_with_norm_mul
parallelogram_law_with_norm 📖	mathematical	—	Real Real.instAdd Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sq parallelogram_law_with_norm_mul
parallelogram_law_with_norm_mul 📖	mathematical	—	Real Real.instAdd Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat inner_self_eq_norm_mul_norm AddMonoidHom.map_add parallelogram_law two_mul
re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat norm_add_mul_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat norm_add_mul_self norm_sub_mul_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instAdd Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat norm_sub_mul_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
re_inner_le_norm 📖	mathematical	—	Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	le_trans RCLike.re_le_norm norm_inner_le_norm
re_inner_self_nonpos 📖	mathematical	—	Real Real.instLE DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	inner_self_eq_norm_sq_to_K RCLike.re_ofReal_pow AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
re_inner_self_pos 📖	mathematical	—	Real Real.instLT Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup	—	inner_self_eq_norm_sq_to_K RCLike.re_ofReal_pow Real.instIsStrictOrderedRing AddGroup.existsAddOfLE
real_inner_I_smul_self 📖	mathematical	—	Inner.inner Real Inner.rclikeToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.I Real.instZero	—	real_inner_eq_re_inner inner_smul_right inner_self_eq_norm_sq_to_K RCLike.mul_re RCLike.I_re RCLike.re_ofReal_pow MulZeroClass.zero_mul RCLike.im_ofReal_pow MulZeroClass.mul_zero sub_self
real_inner_add_add_self 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instAdd Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	inner_conj_symm Nat.instAtLeastTwoHAddOfNat inner_add_add_self instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
real_inner_add_sub_eq_zero_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instZero Norm.norm SeminormedAddCommGroup.toNorm	—	mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing norm_nonneg inner_sub_right inner_add_left real_inner_comm inner_self_eq_norm_mul_norm
real_inner_comm 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike	—	inner_conj_symm
real_inner_div_norm_mul_norm_eq_neg_one_iff 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instNeg Real.instOne Real.instLT Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace	—	neg_eq_iff_eq_neg neg_div inner_neg_right norm_neg real_inner_div_norm_mul_norm_eq_one_iff Function.Surjective.exists neg_surjective Iff.and neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_smul
real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul 📖	mathematical	Real Real.instLT Real.instZero	Real DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instNeg Real.instOne	—	real_inner_smul_self_right norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs mul_assoc mul_comm abs_of_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_mul div_neg_eq_neg_div div_self mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne mul_self_ne_zero norm_ne_zero_iff
real_inner_div_norm_mul_norm_eq_one_iff 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instOne Real.instLT Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace	—	inner_zero_left norm_zero MulZeroClass.zero_mul div_zero NeZero.charZero_one RCLike.charZero_rclike inner_zero_right MulZeroClass.mul_zero div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff inner_eq_norm_mul_iff_div eq_of_div_eq_one real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul
real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul 📖	mathematical	Real Real.instLT Real.instZero	Real DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instOne	—	real_inner_smul_self_right norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs mul_assoc mul_comm abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le div_self mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne' mul_self_ne_zero norm_ne_zero_iff
real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instMul Norm.norm SeminormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.re_to_real re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two
real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instAdd Real.instMul Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.re_to_real re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two
real_inner_eq_re_inner 📖	mathematical	—	Inner.inner Real Inner.rclikeToReal DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re InnerProductSpace.toInner	—	—
real_inner_le_norm 📖	mathematical	—	Real Real.instLE Inner.inner InnerProductSpace.toInner Real.instRCLike Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	le_trans le_abs_self abs_real_inner_le_norm
real_inner_le_one_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Real Real.instLE Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instOne	—	mul_one real_inner_le_norm
real_inner_mem_Icc_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instNeg Real.instOne Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	neg_one_le_real_inner_of_norm_eq_one real_inner_le_one_of_norm_eq_one
real_inner_mul_inner_self_le 📖	mathematical	—	Real Real.instLE Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike	—	real_inner_comm norm_mul NormedDivisionRing.toNormMulClass le_abs_self inner_mul_inner_self_le
real_inner_self_abs 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup Inner.inner InnerProductSpace.toInner Real.instRCLike	—	inner_self_ofReal_norm
real_inner_self_eq_norm_mul_norm 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	inner_self_eq_norm_mul_norm inner_self_eq_norm_sq_to_K
real_inner_self_eq_norm_sq 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike Monoid.toPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm	—	pow_two real_inner_self_eq_norm_mul_norm
real_inner_self_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike	—	inner_self_nonneg
real_inner_self_nonpos 📖	mathematical	—	Real Real.instLE Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	re_inner_self_nonpos
real_inner_self_pos 📖	mathematical	—	Real Real.instLT Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	re_inner_self_pos
real_inner_smul_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul	—	inner_smul_left
real_inner_smul_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul	—	inner_smul_right
real_inner_smul_self_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	real_inner_smul_left real_inner_self_eq_norm_mul_norm
real_inner_smul_self_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instMul Norm.norm SeminormedAddCommGroup.toNorm	—	inner_smul_right real_inner_self_eq_norm_mul_norm
real_inner_sub_sub_self 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instAdd Real.instSub Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	inner_conj_symm Nat.instAtLeastTwoHAddOfNat inner_sub_sub_self instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
sum_inner 📖	mathematical	—	Inner.inner InnerProductSpace.toInner Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass SMulCommClass.symm Algebra.to_smulCommClass

---

← Back to Index