Inner

📁 Source: Mathlib/Analysis/RCLike/Inner.lean

Statistics

Metric	Count
Definitions cWeight, wInner, «term⟪_,_⟫_[_,_]», «term⟪_,_⟫_[_]», «term⟪_,_⟫ₙ_[_]»	5
Theorems abs_wInner_le, conj_wInner_symm, inner_eq_wInner_one, linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero, linearIndependent_of_ne_zero_of_wInner_one_eq_zero, mul_wInner_left, norm_wInner_le, wInner_add_left, wInner_add_right, wInner_cWeight_const_left, wInner_cWeight_const_right, wInner_cWeight_eq_expect, wInner_cWeight_eq_smul_wInner_one, wInner_const_left, wInner_const_right, wInner_neg_left, wInner_neg_right, wInner_nonneg, wInner_of_isEmpty, wInner_one_const_left, wInner_one_const_right, wInner_one_eq_inner, wInner_one_eq_sum, wInner_smul_left, wInner_smul_right, wInner_sub_left, wInner_sub_right, wInner_zero_left, wInner_zero_right	29
Total	34

RCLike

Definitions

Name	Category	Theorems
cWeight 📖	CompOp	8 math math: AddChar.wInner_cWeight_self, wInner_cWeight_eq_expect, AddChar.wInner_cWeight_eq_zero_iff_ne, AddChar.wInner_cWeight_eq_one_iff_eq, wInner_cWeight_const_left, wInner_cWeight_const_right, AddChar.wInner_cWeight_eq_boole, wInner_cWeight_eq_smul_wInner_one
wInner 📖	CompOp	31 math math: AddChar.wInner_cWeight_self, wInner_sub_right, wInner_of_isEmpty, wInner_cWeight_eq_expect, AddChar.wInner_cWeight_eq_zero_iff_ne, wInner_neg_right, mul_wInner_left, abs_wInner_le, wInner_zero_right, wInner_sub_left, wInner_one_eq_inner, wInner_smul_right, AddChar.wInner_cWeight_eq_one_iff_eq, wInner_const_left, wInner_cWeight_const_left, wInner_smul_left, norm_wInner_le, wInner_const_right, conj_wInner_symm, wInner_one_const_right, wInner_zero_left, wInner_neg_left, wInner_one_const_left, wInner_add_left, wInner_one_eq_sum, wInner_cWeight_const_right, AddChar.wInner_cWeight_eq_boole, wInner_nonneg, wInner_add_right, wInner_cWeight_eq_smul_wInner_one, inner_eq_wInner_one
«term⟪_,_⟫_[_,_]» 📖	CompOp	—
«term⟪_,_⟫_[_]» 📖	CompOp	—
«term⟪_,_⟫ₙ_[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_wInner_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero	abs Real.lattice Real.instAddGroup wInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing toInnerProductSpaceReal Pi.instLattice Pi.addGroup	—	norm_wInner_le
conj_wInner_symm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField RingHom.instFunLike starRingEnd toStarRing wInner	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass charZero_rclike SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass Finset.sum_congr conj_smul inner_conj_symm
inner_eq_wInner_one 📖	mathematical	—	Inner.inner PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat InnerProductSpace.toInner PiLp.seminormedAddCommGroup fact_one_le_two_ennreal NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField PiLp.innerProductSpace innerProductSpace wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Pi.instOne Real Real.instOne WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal Finset.sum_congr one_smul
linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero 📖	mathematical	Pairwise wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace cWeight MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Pi.Function.module NormedSpace.toModule InnerProductSpace.toNormedSpace	—	isEmpty_or_nonempty Unique.instSubsingleton linearIndependent_empty_type linearIndependent_of_ne_zero_of_wInner_one_eq_zero charZero_rclike wInner_cWeight_eq_smul_wInner_one NNRat.cast_smul_eq_nnqsmul IsScalarTower.right NNRat.cast_inv NNRat.cast_natCast NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
linearIndependent_of_ne_zero_of_wInner_one_eq_zero 📖	mathematical	Pairwise wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace Pi.instOne Real Real.instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Pi.Function.module NormedSpace.toModule InnerProductSpace.toNormedSpace	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal linearIndependent_of_ne_zero_of_inner_eq_zero Iff.ne WithLp.toLp_eq_zero wInner_one_eq_inner RingHomInvPair.ids LinearMap.linearIndependent_iff_of_injOn Function.Injective.injOn WithLp.toLp_injective
mul_wInner_left 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField wInner Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid toStarRing	—	wInner_smul_left StarMul.toStarModule Algebra.to_smulCommClass IsScalarTower.left star_star smul_eq_mul
norm_wInner_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero	Norm.norm NormedField.toNorm DenselyNormedField.toNormedField toDenselyNormedField wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing innerProductSpace Real.instRCLike Real.normedCommRing toInnerProductSpaceReal	—	LE.le.trans_eq norm_sum_le Finset.sum_congr Algebra.smul_def norm_mul NormedDivisionRing.toNormMulClass norm_algebraMap' NormedDivisionRing.to_normOneClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_conj conj_trivial instTrivialStarReal
wInner_add_left 📖	mathematical	—	wInner Pi.instAdd 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 toDenselyNormedField	—	Finset.sum_congr inner_add_left smul_add Finset.sum_add_distrib
wInner_add_right 📖	mathematical	—	wInner Pi.instAdd 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 toDenselyNormedField	—	Finset.sum_congr inner_add_right smul_add Finset.sum_add_distrib
wInner_cWeight_const_left 📖	mathematical	—	wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace cWeight Finset.expect ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DivisionSemiring.toNNRatAlgebra charZero_rclike Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike starRingEnd toStarRing	—	charZero_rclike wInner_cWeight_eq_expect Finset.expect_congr
wInner_cWeight_const_right 📖	mathematical	—	wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace cWeight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Finset.expect ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DivisionSemiring.toNNRatAlgebra charZero_rclike Finset.univ DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike starRingEnd toStarRing	—	charZero_rclike wInner_cWeight_eq_expect Finset.expect_congr Finset.mul_expect Algebra.to_smulCommClass
wInner_cWeight_eq_expect 📖	mathematical	—	wInner cWeight Finset.expect ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DivisionSemiring.toNNRatAlgebra charZero_rclike Finset.univ Inner.inner InnerProductSpace.toInner	—	charZero_rclike Finset.sum_congr NNRat.cast_smul_eq_nnqsmul IsScalarTower.nnrat NNRat.cast_inv NNRat.cast_natCast Finset.smul_sum
wInner_cWeight_eq_smul_wInner_one 📖	mathematical	—	wInner cWeight NNRat Algebra.toSMul instCommSemiringNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField DivisionSemiring.toNNRatAlgebra charZero_rclike NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNRat.instSemifield Fintype.card Pi.instOne Real Real.instOne	—	charZero_rclike Finset.sum_congr one_smul NNRat.cast_smul_eq_nnqsmul IsScalarTower.nnrat NNRat.cast_inv NNRat.cast_natCast Finset.smul_sum
wInner_const_left 📖	mathematical	—	wInner 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 Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.univ Real Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra toNormedAlgebra DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike starRingEnd toStarRing	—	Finset.sum_congr Finset.sum_mul Algebra.smul_mul_assoc
wInner_const_right 📖	mathematical	—	wInner 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 Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.univ Real Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra toNormedAlgebra DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike starRingEnd toStarRing	—	Finset.sum_congr Finset.mul_sum Algebra.mul_smul_comm
wInner_neg_left 📖	mathematical	—	wInner Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	Finset.sum_congr inner_neg_left smul_neg Finset.sum_neg_distrib
wInner_neg_right 📖	mathematical	—	wInner Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	Finset.sum_congr inner_neg_right smul_neg Finset.sum_neg_distrib
wInner_nonneg 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Preorder.toLE PartialOrder.toPreorder toPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing innerProductSpace	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono toIsOrderedAddMonoid smul_nonneg IsOrderedModule.toPosSMulMono instIsOrderedModule toStarOrderedRing instStarModuleReal IsScalarTower.right Algebra.to_smulCommClass mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing toIsStrictOrderedRing star_nonneg_iff
wInner_of_isEmpty 📖	mathematical	—	wInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	Unique.instSubsingleton wInner_zero_left
wInner_one_const_left 📖	mathematical	—	wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace Pi.instOne Real Real.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.univ DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	wInner_one_eq_sum Finset.sum_congr Finset.sum_mul
wInner_one_const_right 📖	mathematical	—	wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace Pi.instOne Real Real.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.univ DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd toStarRing	—	wInner_one_eq_sum Finset.sum_congr Finset.mul_sum
wInner_one_eq_inner 📖	mathematical	—	wInner NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField innerProductSpace Pi.instOne Real Real.instOne Inner.inner WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat InnerProductSpace.toInner PiLp.seminormedAddCommGroup fact_one_le_two_ennreal NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PiLp.innerProductSpace WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal Finset.sum_congr one_smul
wInner_one_eq_sum 📖	mathematical	—	wInner Pi.instOne Real Real.instOne Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Finset.univ Inner.inner InnerProductSpace.toInner	—	Finset.sum_congr one_smul
wInner_smul_left 📖	mathematical	IsScalarTower Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace CommSemiring.toSemiring	wInner Pi.instSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid	—	Finset.sum_congr inner_smul_left_eq_star_smul Finset.smul_sum SMulCommClass.smul_comm
wInner_smul_right 📖	mathematical	IsScalarTower Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace CommSemiring.toSemiring	wInner Pi.instSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Finset.sum_congr inner_smul_right_eq_smul Finset.smul_sum SMulCommClass.smul_comm instSMulCommClass
wInner_sub_left 📖	mathematical	—	wInner Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	sub_eq_add_neg wInner_add_left wInner_neg_left
wInner_sub_right 📖	mathematical	—	wInner Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	sub_eq_add_neg wInner_add_right wInner_neg_right
wInner_zero_left 📖	mathematical	—	wInner Pi.instZero 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 toDenselyNormedField	—	Finset.sum_congr inner_zero_left smul_zero Finset.sum_const_zero
wInner_zero_right 📖	mathematical	—	wInner Pi.instZero 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 toDenselyNormedField	—	Finset.sum_congr inner_zero_right smul_zero Finset.sum_const_zero

---

← Back to Index