OperatorNorm

📁 Source: Mathlib/Analysis/Complex/OperatorNorm.lean

Statistics

Metric	Count
Definitions	0
Theorems conjCLE_enorm, conjCLE_nnorm, conjCLE_norm, det_conjLIE, imCLM_enorm, imCLM_nnnorm, imCLM_norm, linearEquiv_det_conjLIE, ofRealCLM_enorm, ofRealCLM_nnnorm, ofRealCLM_norm, reCLM_enorm, reCLM_nnnorm, reCLM_norm	14
Total	14

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjCLE_enorm 📖	mathematical	—	ENorm.enorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids Real.normedCommRing SeminormedAddGroup.toContinuousENorm ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids conjCLE ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	RingHomIsometric.ids RingHomInvPair.ids conjCLE_norm ENNReal.ofReal_one
conjCLE_nnorm 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids Real.normedCommRing ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids conjCLE NNReal instOneNNReal	—	RingHomIsometric.ids RingHomInvPair.ids conjCLE_norm
conjCLE_norm 📖	mathematical	—	Norm.norm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids conjCLE Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap instNontrivial RingHomIsometric.ids RingHomInvPair.ids
det_conjLIE 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring Complex AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap Real.semiring RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv conjLIE Real.instNeg Real.instOne	—	det_conjAe
imCLM_enorm 📖	mathematical	—	ENorm.enorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField RingHomIsometric.ids SeminormedAddGroup.toContinuousENorm imCLM ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	RingHomIsometric.ids imCLM_norm ENNReal.ofReal_one
imCLM_nnnorm 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField RingHomIsometric.ids imCLM NNReal instOneNNReal	—	RingHomIsometric.ids imCLM_norm
imCLM_norm 📖	mathematical	—	Norm.norm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField imCLM Real.instOne	—	le_antisymm LinearMap.mkContinuous_norm_le zero_le_one Real.instZeroLEOneClass CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass ContinuousLinearMap.unit_le_opNorm RingHomIsometric.ids norm_I
linearEquiv_det_conjLIE 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det LinearIsometryEquiv.toLinearEquiv Real.semiring conjLIE Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Units.instOne	—	linearEquiv_det_conjAe
ofRealCLM_enorm 📖	mathematical	—	ENorm.enorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField RingHomIsometric.ids SeminormedAddGroup.toContinuousENorm ofRealCLM ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	RingHomIsometric.ids ofRealCLM_norm ENNReal.ofReal_one
ofRealCLM_nnnorm 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField RingHomIsometric.ids ofRealCLM NNReal instOneNNReal	—	RingHomIsometric.ids ofRealCLM_norm
ofRealCLM_norm 📖	mathematical	—	Norm.norm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedSpace.complexToReal ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField ofRealCLM Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap Real.instNontrivial RingHomIsometric.ids
reCLM_enorm 📖	mathematical	—	ENorm.enorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField RingHomIsometric.ids SeminormedAddGroup.toContinuousENorm reCLM ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	RingHomIsometric.ids reCLM_norm ENNReal.ofReal_one
reCLM_nnnorm 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField RingHomIsometric.ids reCLM NNReal instOneNNReal	—	RingHomIsometric.ids reCLM_norm
reCLM_norm 📖	mathematical	—	Norm.norm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField reCLM Real.instOne	—	le_antisymm LinearMap.mkContinuous_norm_le zero_le_one Real.instZeroLEOneClass CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass ContinuousLinearMap.unit_le_opNorm RingHomIsometric.ids RCLike.instCStarRing instNontrivial

---

← Back to Index