Extend

📁 Source: Mathlib/Analysis/Normed/Module/RCLike/Extend.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_extendTo𝕜, norm_extendTo𝕜', norm_extendTo𝕜'_bound	3
Total	3

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_extendTo𝕜 📖	mathematical	—	Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring extendTo𝕜 Real Real.semiring Real.pseudoMetricSpace RestrictScalars instSeminormedAddCommGroupRestrictScalars instAddCommMonoidRestrictScalars RestrictScalars.module Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Real.normedCommRing Real.denselyNormedField RestrictScalars.normedSpace	—	norm_extendTo𝕜'
norm_extendTo𝕜' 📖	mathematical	—	Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring extendTo𝕜' Real Real.semiring Real.pseudoMetricSpace Real.normedField Real.normedCommRing Real.denselyNormedField	—	le_antisymm opNorm_le_bound norm_nonneg RingHomIsometric.ids norm_extendTo𝕜'_bound LinearMap.extendTo𝕜'_apply_re RCLike.abs_re_le_norm le_opNorm
norm_extendTo𝕜'_bound 📖	mathematical	—	Real Real.instLE Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule extendTo𝕜' Real.instMul Real.semiring Real.pseudoMetricSpace Real.normedField hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toNorm	—	norm_zero mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg RingHomIsometric.ids mul_le_mul_iff_right₀ PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff sq LinearMap.norm_extendTo𝕜'_apply_sq le_abs_self le_opNorm norm_smul NormedSpace.toNormSMulClass RCLike.norm_conj mul_left_comm

---

← Back to Index