TensorProduct

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

Statistics

Metric	Count
Definitions lTensor, rTensor, lTensor, rTensor, tensorProduct, assocIsometry, commIsometry, congrIsometry, instInner, instInnerProductSpace, instNormedAddCommGroup, lidIsometry, mapInclIsometry, mapIsometry	14
Theorems lTensor_apply, lTensor_def, rTensor_apply, rTensor_def, toLinearMap_lTensor, toLinearMap_rTensor, lTensor_apply, lTensor_def, rTensor_apply, rTensor_def, symm_lTensor, symm_rTensor, toLinearEquiv_lTensor, toLinearEquiv_rTensor, toLinearIsometry_lTensor, toLinearIsometry_rTensor, adjoint_lTensor, adjoint_rTensor, basisTensorProduct, tmul, tensorProduct_apply, tensorProduct_apply', tensorProduct_repr_tmul_apply, tensorProduct_repr_tmul_apply', toBasis_tensorProduct, inner_tmul_eq, adjoint_map, assocIsometry_apply, assocIsometry_symm_apply, commIsometry_apply, commIsometry_symm, congrIsometry_apply, congrIsometry_refl_refl, congrIsometry_symm, dist_tmul_le, edist_tmul_le, enorm_assoc, enorm_comm, enorm_lid, enorm_map, enorm_tmul, ext_iff_inner_left, ext_iff_inner_left_threefold, ext_iff_inner_left_threefold', ext_iff_inner_right, ext_iff_inner_right_threefold, ext_iff_inner_right_threefold', inner_assoc_assoc, inner_comm_comm, inner_lid_lid, inner_mapIncl_mapIncl, inner_map_map, inner_tmul, lidIsometry_apply, lidIsometry_symm_apply, mapInclIsometry_apply, mapIsometry_apply, mapIsometry_id_id, nndist_tmul_le, nnnorm_assoc, nnnorm_comm, nnnorm_lid, nnnorm_map, nnnorm_tmul, norm_assoc, norm_comm, norm_lid, norm_map, norm_tmul, toLinearEquiv_assocIsometry, toLinearEquiv_commIsometry, toLinearEquiv_congrIsometry, toLinearEquiv_lidIsometry, toLinearMap_mapInclIsometry, toLinearMap_mapIsometry	75
Total	89

LinearIsometry

Definitions

Name	Category	Theorems
lTensor 📖	CompOp	4 math math: lTensor_apply, LinearIsometryEquiv.toLinearIsometry_lTensor, toLinearMap_lTensor, lTensor_def
rTensor 📖	CompOp	4 math math: rTensor_def, toLinearMap_rTensor, LinearIsometryEquiv.toLinearIsometry_rTensor, rTensor_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule instFunLike lTensor LinearMap CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup TensorProduct.addCommMonoid LinearMap.instFunLike LinearMap.lTensor toLinearMap	—	—
lTensor_def 📖	mathematical	—	lTensor TensorProduct.mapIsometry id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	—	—
rTensor_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule instFunLike rTensor LinearMap CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup TensorProduct.addCommMonoid LinearMap.instFunLike LinearMap.rTensor toLinearMap	—	—
rTensor_def 📖	mathematical	—	rTensor TensorProduct.mapIsometry id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	—	—
toLinearMap_lTensor 📖	mathematical	—	toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule lTensor LinearMap.lTensor AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
toLinearMap_rTensor 📖	mathematical	—	toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule rTensor LinearMap.rTensor AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—

LinearIsometryEquiv

Definitions

Name	Category	Theorems
lTensor 📖	CompOp	5 math math: lTensor_apply, toLinearEquiv_lTensor, lTensor_def, toLinearIsometry_lTensor, symm_lTensor
rTensor 📖	CompOp	5 math math: rTensor_apply, symm_rTensor, toLinearIsometry_rTensor, toLinearEquiv_rTensor, rTensor_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule EquivLike.toFunLike instEquivLike lTensor LinearEquiv CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup TensorProduct.addCommMonoid DFinsupp.instEquivLikeLinearEquiv LinearEquiv.lTensor toLinearEquiv	—	RingHomInvPair.ids
lTensor_def 📖	mathematical	—	lTensor TensorProduct.congrIsometry refl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	—	RingHomInvPair.ids
rTensor_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule EquivLike.toFunLike instEquivLike rTensor LinearEquiv CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup TensorProduct.addCommMonoid DFinsupp.instEquivLikeLinearEquiv LinearEquiv.rTensor toLinearEquiv	—	RingHomInvPair.ids
rTensor_def 📖	mathematical	—	rTensor TensorProduct.congrIsometry refl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	—	RingHomInvPair.ids
symm_lTensor 📖	mathematical	—	symm TensorProduct Semifield.toCommSemiring 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.instNormedAddCommGroup TensorProduct.instModule lTensor	—	RingHomInvPair.ids
symm_rTensor 📖	mathematical	—	symm TensorProduct Semifield.toCommSemiring 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.instNormedAddCommGroup TensorProduct.instModule rTensor	—	RingHomInvPair.ids
toLinearEquiv_lTensor 📖	mathematical	—	toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule lTensor LinearEquiv.lTensor AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids
toLinearEquiv_rTensor 📖	mathematical	—	toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instModule rTensor LinearEquiv.rTensor AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids
toLinearIsometry_lTensor 📖	mathematical	—	toLinearIsometry TensorProduct Semifield.toCommSemiring 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.instNormedAddCommGroup TensorProduct.instModule lTensor LinearIsometry.lTensor	—	RingHomInvPair.ids
toLinearIsometry_rTensor 📖	mathematical	—	toLinearIsometry TensorProduct Semifield.toCommSemiring 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.instNormedAddCommGroup TensorProduct.instModule rTensor LinearIsometry.rTensor	—	RingHomInvPair.ids

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoint_lTensor 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace addCommMonoid module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv adjoint Module.Finite.tensorProduct lTensor	—	RingHomInvPair.instStarRingEnd smulCommClass_self Module.Finite.tensorProduct TensorProduct.adjoint_map IsSymmetric.adjoint_eq
adjoint_rTensor 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace addCommMonoid module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv adjoint Module.Finite.tensorProduct rTensor	—	RingHomInvPair.instStarRingEnd smulCommClass_self Module.Finite.tensorProduct TensorProduct.adjoint_map IsSymmetric.adjoint_eq

Orthonormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisTensorProduct 📖	mathematical	Orthonormal NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.Basis.instFunLike	TensorProduct Semifield.toCommSemiring TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Basis.tensorProduct	—	IsScalarTower.to_smulCommClass IsScalarTower.left Module.Basis.tensorProduct_apply' tmul
tmul 📖	mathematical	Orthonormal NormedAddCommGroup.toSeminormedAddCommGroup	TensorProduct Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace TensorProduct.tmul	—	orthonormal_iff_ite mul_ite mul_one MulZeroClass.mul_zero

OrthonormalBasis

Definitions

Name	Category	Theorems
tensorProduct 📖	CompOp	5 math math: toBasis_tensorProduct, tensorProduct_repr_tmul_apply', tensorProduct_apply', tensorProduct_apply, tensorProduct_repr_tmul_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorProduct_apply 📖	mathematical	—	DFunLike.coe OrthonormalBasis TensorProduct Semifield.toCommSemiring 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 TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace instFintypeProd instFunLike tensorProduct TensorProduct.tmul	—	Module.Basis.coe_toOrthonormalBasis Module.Basis.tensorProduct_apply
tensorProduct_apply' 📖	mathematical	—	DFunLike.coe OrthonormalBasis TensorProduct Semifield.toCommSemiring 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 TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace instFintypeProd instFunLike tensorProduct TensorProduct.tmul	—	tensorProduct_apply
tensorProduct_repr_tmul_apply 📖	mathematical	—	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace EuclideanSpace TensorProduct.instNormedAddCommGroup PiLp.seminormedAddCommGroup fact_one_le_two_ennreal instFintypeProd NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing TensorProduct.instInnerProductSpace WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing RCLike.innerProductSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike repr tensorProduct TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	RingHomInvPair.ids fact_one_le_two_ennreal IsScalarTower.to_smulCommClass Module.Basis.tensorProduct_repr_tmul_apply coe_toBasis_repr_apply
tensorProduct_repr_tmul_apply' 📖	mathematical	—	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace EuclideanSpace TensorProduct.instNormedAddCommGroup PiLp.seminormedAddCommGroup fact_one_le_two_ennreal instFintypeProd NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing TensorProduct.instInnerProductSpace WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing RCLike.innerProductSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike repr tensorProduct TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	tensorProduct_repr_tmul_apply
toBasis_tensorProduct 📖	mathematical	—	toBasis TensorProduct Semifield.toCommSemiring 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 TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace instFintypeProd tensorProduct Module.Basis.tensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left IsScalarTower.to_smulCommClass Module.Basis.toBasis_toOrthonormalBasis

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_tmul_eq 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField 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 NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace innerProductSpace TensorProduct.instInner TensorProduct.tmul InnerProductSpace.toInner Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul

TensorProduct

Definitions

Name	Category	Theorems
assocIsometry 📖	CompOp	3 math math: assocIsometry_apply, toLinearEquiv_assocIsometry, assocIsometry_symm_apply
commIsometry 📖	CompOp	3 math math: toLinearEquiv_commIsometry, commIsometry_symm, commIsometry_apply
congrIsometry 📖	CompOp	6 math math: congrIsometry_refl_refl, toLinearEquiv_congrIsometry, congrIsometry_symm, LinearIsometryEquiv.lTensor_def, congrIsometry_apply, LinearIsometryEquiv.rTensor_def
instInner 📖	CompOp	13 math math: inner_tmul, ext_iff_inner_left, ext_iff_inner_right_threefold', ext_iff_inner_left_threefold', ext_iff_inner_left_threefold, inner_lid_lid, inner_mapIncl_mapIncl, ext_iff_inner_right, RCLike.inner_tmul_eq, inner_assoc_assoc, inner_comm_comm, ext_iff_inner_right_threefold, inner_map_map
instInnerProductSpace 📖	CompOp	23 math math: Pi.comul_eq_adjoint, OrthonormalBasis.toBasis_tensorProduct, ext_iff_inner_right_threefold', adjoint_map, Orthonormal.basisTensorProduct, LinearMap.adjoint_rTensor, ext_iff_inner_left_threefold', ext_iff_inner_left_threefold, OrthonormalBasis.tensorProduct_repr_tmul_apply', norm_assoc, InnerProductSpace.AlgebraOfCoalgebra.mul_def, inner_assoc_assoc, OrthonormalBasis.tensorProduct_apply', LinearMap.adjoint_lTensor, assocIsometry_apply, enorm_assoc, toLinearEquiv_assocIsometry, nnnorm_assoc, OrthonormalBasis.tensorProduct_apply, Orthonormal.tmul, ext_iff_inner_right_threefold, OrthonormalBasis.tensorProduct_repr_tmul_apply, assocIsometry_symm_apply
instNormedAddCommGroup 📖	CompOp	65 math math: Pi.comul_eq_adjoint, mapInclIsometry_apply, enorm_lid, OrthonormalBasis.toBasis_tensorProduct, congrIsometry_refl_refl, enorm_comm, ext_iff_inner_right_threefold', toLinearEquiv_lidIsometry, adjoint_map, LinearIsometryEquiv.lTensor_apply, mapIsometry_id_id, Orthonormal.basisTensorProduct, lidIsometry_apply, LinearMap.adjoint_rTensor, ext_iff_inner_left_threefold', LinearIsometry.lTensor_apply, ext_iff_inner_left_threefold, norm_comm, OrthonormalBasis.tensorProduct_repr_tmul_apply', norm_assoc, nnnorm_tmul, InnerProductSpace.AlgebraOfCoalgebra.mul_def, nnnorm_map, toLinearEquiv_congrIsometry, toLinearEquiv_commIsometry, enorm_tmul, inner_assoc_assoc, LinearIsometryEquiv.toLinearEquiv_lTensor, OrthonormalBasis.tensorProduct_apply', LinearMap.adjoint_lTensor, assocIsometry_apply, LinearIsometryEquiv.rTensor_apply, LinearIsometry.toLinearMap_rTensor, LinearIsometryEquiv.symm_rTensor, commIsometry_symm, enorm_assoc, dist_tmul_le, norm_lid, toLinearEquiv_assocIsometry, nnnorm_assoc, mapIsometry_apply, toLinearMap_mapIsometry, enorm_map, commIsometry_apply, congrIsometry_symm, LinearIsometryEquiv.toLinearIsometry_rTensor, norm_tmul, nnnorm_comm, norm_map, LinearIsometryEquiv.toLinearEquiv_rTensor, LinearIsometryEquiv.toLinearIsometry_lTensor, LinearIsometry.rTensor_apply, LinearIsometry.toLinearMap_lTensor, nndist_tmul_le, OrthonormalBasis.tensorProduct_apply, congrIsometry_apply, nnnorm_lid, Orthonormal.tmul, LinearIsometryEquiv.symm_lTensor, ext_iff_inner_right_threefold, OrthonormalBasis.tensorProduct_repr_tmul_apply, assocIsometry_symm_apply, toLinearMap_mapInclIsometry, lidIsometry_symm_apply, edist_tmul_le
lidIsometry 📖	CompOp	3 math math: toLinearEquiv_lidIsometry, lidIsometry_apply, lidIsometry_symm_apply
mapInclIsometry 📖	CompOp	2 math math: mapInclIsometry_apply, toLinearMap_mapInclIsometry
mapIsometry 📖	CompOp	5 math math: LinearIsometry.rTensor_def, mapIsometry_id_id, mapIsometry_apply, toLinearMap_mapIsometry, LinearIsometry.lTensor_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoint_map 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instInnerProductSpace LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.adjoint Module.Finite.tensorProduct map	—	ext' RingHomInvPair.instStarRingEnd smulCommClass_self Module.Finite.tensorProduct LinearMap.adjoint_inner_left
assocIsometry_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule instNormedAddCommGroup instInnerProductSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike assocIsometry LinearEquiv CommSemiring.toSemiring DFinsupp.instEquivLikeLinearEquiv assoc	—	RingHomInvPair.ids
assocIsometry_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule instNormedAddCommGroup instInnerProductSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm assocIsometry LinearEquiv CommSemiring.toSemiring DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm assoc	—	RingHomInvPair.ids
commIsometry_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike commIsometry LinearEquiv CommSemiring.toSemiring addCommMonoid DFinsupp.instEquivLikeLinearEquiv comm	—	RingHomInvPair.ids
commIsometry_symm 📖	mathematical	—	LinearIsometryEquiv.symm TensorProduct Semifield.toCommSemiring 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instNormedAddCommGroup instModule commIsometry	—	RingHomInvPair.ids
congrIsometry_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike congrIsometry LinearEquiv CommSemiring.toSemiring addCommMonoid DFinsupp.instEquivLikeLinearEquiv congr SemilinearEquivClass.semilinearEquiv SemilinearIsometryEquivClass.toSemilinearEquivClass LinearIsometryEquiv.instSemilinearIsometryEquivClass	—	RingHomInvPair.ids
congrIsometry_refl_refl 📖	mathematical	—	congrIsometry LinearIsometryEquiv.refl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instModule	—	RingHomInvPair.ids AlgebraTensorModule.curry_injective IsScalarTower.left isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass
congrIsometry_symm 📖	mathematical	—	LinearIsometryEquiv.symm TensorProduct Semifield.toCommSemiring 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instNormedAddCommGroup instModule congrIsometry	—	RingHomInvPair.ids
dist_tmul_le 📖	mathematical	—	Real Real.instLE Dist.dist TensorProduct Semifield.toCommSemiring 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 PseudoMetricSpace.toDist instNormedAddCommGroup tmul Real.instAdd Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	dist_eq_norm le_imp_le_of_le_of_le norm_sub_le le_refl norm_tmul
edist_tmul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist TensorProduct Semifield.toCommSemiring 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 PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instNormedAddCommGroup tmul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm	—	edist_eq_enorm_sub le_imp_le_of_le_of_le enorm_sub_le le_refl enorm_tmul
enorm_assoc 📖	mathematical	—	ENorm.enorm TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup instInnerProductSpace SeminormedAddGroup.toContinuousENorm DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv assoc	—	LinearIsometry.enorm_map RingHomInvPair.ids
enorm_comm 📖	mathematical	—	ENorm.enorm TensorProduct Semifield.toCommSemiring 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 ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv comm	—	LinearIsometry.enorm_map RingHomInvPair.ids
enorm_lid 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toModule NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv lid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace instNormedAddCommGroup	—	LinearIsometry.enorm_map RingHomInvPair.ids
enorm_map 📖	mathematical	—	ENorm.enorm TensorProduct Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring addCommMonoid instModule LinearMap.instFunLike map LinearIsometry.toLinearMap ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	LinearIsometry.enorm_map
enorm_tmul 📖	mathematical	—	ENorm.enorm TensorProduct Semifield.toCommSemiring 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 ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup SeminormedAddGroup.toContinuousENorm tmul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	nnnorm_tmul
ext_iff_inner_left 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 instInner tmul	—	inner_conj_symm ext_iff_inner_right
ext_iff_inner_left_threefold 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule instInner instNormedAddCommGroup instInnerProductSpace tmul	—	inner_conj_symm ext_iff_inner_right_threefold
ext_iff_inner_left_threefold' 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule instInner instNormedAddCommGroup instInnerProductSpace tmul	—	inner_conj_symm ext_iff_inner_right_threefold'
ext_iff_inner_right 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 instInner tmul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ext'
ext_iff_inner_right_threefold 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule instInner instNormedAddCommGroup instInnerProductSpace tmul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ext_threefold
ext_iff_inner_right_threefold' 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule instInner instNormedAddCommGroup instInnerProductSpace tmul	—	RingHomInvPair.ids LinearIsometryEquiv.injective LinearIsometryEquiv.inner_map_eq_flip
inner_assoc_assoc 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule instInner instNormedAddCommGroup instInnerProductSpace DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv assoc	—	induction_on RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass inner_zero_left inner_zero_right zero_tmul mul_assoc add_tmul map_add SemilinearMapClass.toAddHomClass inner_add_right inner_add_left
inner_comm_comm 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 instInner DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv comm	—	induction_on RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass inner_zero_left inner_zero_right mul_comm map_add SemilinearMapClass.toAddHomClass inner_add_right inner_add_left
inner_lid_lid 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toModule NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv lid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace instInner	—	induction_on RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass inner_zero_left inner_zero_right inner_smul_right inner_smul_left mul_assoc map_add SemilinearMapClass.toAddHomClass inner_add_right inner_add_left
inner_mapIncl_mapIncl 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 instInner DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module addCommMonoid instModule LinearMap.instFunLike mapIncl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace	—	inner_map_map
inner_map_map 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace instInner DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring addCommMonoid instModule LinearMap.instFunLike map LinearIsometry.toLinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Algebra.to_smulCommClass LinearIsometry.inner_map_map map_add SemilinearMapClass.toAddHomClass
inner_tmul 📖	mathematical	—	Inner.inner TensorProduct Semifield.toCommSemiring 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 instInner tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing InnerProductSpace.toInner	—	—
lidIsometry_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace instNormedAddCommGroup instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike lidIsometry LinearEquiv CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid DFinsupp.instEquivLikeLinearEquiv lid	—	RingHomInvPair.ids
lidIsometry_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace instNormedAddCommGroup instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm lidIsometry tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	RingHomInvPair.ids
mapInclIsometry_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module instNormedAddCommGroup Submodule.normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace instModule LinearIsometry.instFunLike mapInclIsometry LinearMap CommSemiring.toSemiring addCommMonoid LinearMap.instFunLike mapIncl	—	—
mapIsometry_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instModule LinearIsometry.instFunLike mapIsometry LinearMap CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup addCommMonoid LinearMap.instFunLike map LinearIsometry.toLinearMap	—	—
mapIsometry_id_id 📖	mathematical	—	mapIsometry LinearIsometry.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instModule	—	LinearIsometry.ext map_id
nndist_tmul_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNDist.nndist TensorProduct Semifield.toCommSemiring 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 PseudoMetricSpace.toNNDist instNormedAddCommGroup tmul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toMul NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	nndist_eq_nnnorm le_imp_le_of_le_of_le nnnorm_sub_le le_refl nnnorm_tmul
nnnorm_assoc 📖	mathematical	—	NNNorm.nnnorm TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup instInnerProductSpace DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv assoc	—	LinearIsometryEquiv.nnnorm_map RingHomInvPair.ids
nnnorm_comm 📖	mathematical	—	NNNorm.nnnorm TensorProduct Semifield.toCommSemiring 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 SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv comm	—	LinearIsometryEquiv.nnnorm_map RingHomInvPair.ids
nnnorm_lid 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toModule NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv lid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace instNormedAddCommGroup	—	LinearIsometryEquiv.nnnorm_map RingHomInvPair.ids
nnnorm_map 📖	mathematical	—	NNNorm.nnnorm TensorProduct Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring addCommMonoid instModule LinearMap.instFunLike map LinearIsometry.toLinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	LinearIsometry.nnnorm_map
nnnorm_tmul 📖	mathematical	—	NNNorm.nnnorm TensorProduct Semifield.toCommSemiring 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 SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instNormedAddCommGroup tmul NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	norm_tmul
norm_assoc 📖	mathematical	—	Norm.norm TensorProduct Semifield.toCommSemiring 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 addCommMonoid instModule NormedAddCommGroup.toNorm instNormedAddCommGroup instInnerProductSpace DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv assoc	—	LinearIsometryEquiv.norm_map RingHomInvPair.ids
norm_comm 📖	mathematical	—	Norm.norm TensorProduct Semifield.toCommSemiring 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 NormedAddCommGroup.toNorm instNormedAddCommGroup DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv comm	—	LinearIsometryEquiv.norm_map RingHomInvPair.ids
norm_lid 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toModule NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv lid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace instNormedAddCommGroup	—	LinearIsometryEquiv.norm_map RingHomInvPair.ids
norm_map 📖	mathematical	—	Norm.norm TensorProduct Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace NormedAddCommGroup.toNorm instNormedAddCommGroup DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring addCommMonoid instModule LinearMap.instFunLike map LinearIsometry.toLinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	LinearIsometry.norm_map
norm_tmul 📖	mathematical	—	Norm.norm TensorProduct Semifield.toCommSemiring 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 NormedAddCommGroup.toNorm instNormedAddCommGroup tmul Real Real.instMul	—	inner_self_eq_norm_sq_to_K RCLike.re_ofReal_pow Real.sqrt_sq RCLike.mul_re RCLike.im_ofReal_pow MulZeroClass.mul_zero sub_zero Real.sqrt_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing inner_tmul
toLinearEquiv_assocIsometry 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid instModule instNormedAddCommGroup instInnerProductSpace assocIsometry assoc	—	RingHomInvPair.ids
toLinearEquiv_commIsometry 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instModule commIsometry comm	—	RingHomInvPair.ids
toLinearEquiv_congrIsometry 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instModule congrIsometry congr AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids
toLinearEquiv_lidIsometry 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace instNormedAddCommGroup instModule lidIsometry lid	—	RingHomInvPair.ids
toLinearMap_mapInclIsometry 📖	mathematical	—	LinearIsometry.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module instNormedAddCommGroup Submodule.normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace instModule mapInclIsometry mapIncl	—	—
toLinearMap_mapIsometry 📖	mathematical	—	LinearIsometry.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instNormedAddCommGroup instModule mapIsometry map AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—

---

← Back to Index