Extend

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

Statistics

Metric	Count
Definitions extendTo𝕜, extendTo𝕜', extendTo𝕜, extendTo𝕜', instNormedSpaceRestrictScalarsReal	5
Theorems extendTo𝕜'_apply, extendTo𝕜_apply, extendTo𝕜'_apply, extendTo𝕜'_apply_re, extendTo𝕜_apply, norm_extendTo𝕜'_apply_sq	6
Total	11

ContinuousLinearMap

Definitions

Name	Category	Theorems
extendTo𝕜 📖	CompOp	2 math math: norm_extendTo𝕜, extendTo𝕜_apply
extendTo𝕜' 📖	CompOp	3 math math: norm_extendTo𝕜'_bound, norm_extendTo𝕜', extendTo𝕜'_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendTo𝕜'_apply 📖	mathematical	—	DFunLike.coe 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 funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule extendTo𝕜' SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing RCLike.ofReal Real Real.semiring Real.pseudoMetricSpace Real.normedField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing RCLike.I SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
extendTo𝕜_apply 📖	mathematical	—	DFunLike.coe 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 funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule extendTo𝕜 SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing RCLike.ofReal Real Real.semiring Real.pseudoMetricSpace RestrictScalars instSeminormedAddCommGroupRestrictScalars instAddCommMonoidRestrictScalars RestrictScalars.module Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing RCLike.I SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—

LinearMap

Definitions

Name	Category	Theorems
extendTo𝕜 📖	CompOp	1 math math: extendTo𝕜_apply
extendTo𝕜' 📖	CompOp	3 math math: extendTo𝕜'_apply, extendTo𝕜'_apply_re, norm_extendTo𝕜'_apply_sq
instNormedSpaceRestrictScalarsReal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendTo𝕜'_apply 📖	mathematical	—	DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id extendTo𝕜' SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing RCLike.ofReal Real Real.semiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing RCLike.I SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
extendTo𝕜'_apply_re 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id extendTo𝕜' Real.semiring	—	map_sub AddMonoidHom.instAddMonoidHomClass RCLike.ofReal_re RCLike.mul_re RCLike.I_re MulZeroClass.zero_mul RCLike.ofReal_im MulZeroClass.mul_zero sub_zero
extendTo𝕜_apply 📖	mathematical	—	DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id extendTo𝕜 SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing RCLike.ofReal LinearMap Real Real.semiring RestrictScalars instAddCommMonoidRestrictScalars Real.instAddCommMonoid RestrictScalars.module Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing RCLike.I SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
norm_extendTo𝕜'_apply_sq 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id extendTo𝕜' Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction RingHom CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike starRingEnd RCLike.toStarRing	—	RCLike.conj_mul RCLike.ofReal_pow RCLike.ofReal_re smul_eq_mul map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass extendTo𝕜'_apply_re

---

← Back to Index