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 NNReal.instOne	—	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 addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.complexToReal NormedField.toNormedSpace MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap Real.semiring RingHomInvPair.ids SeminormedAddCommGroup.toAddCommGroup 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 NNReal.instOne	—	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 instReflLe
linearEquiv_det_conjLIE 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddCommGroup.toAddCommMonoid addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField 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 NNReal.instOne	—	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 NNReal.instOne	—	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 instReflLe

---

← Back to Index