Span

📁 Source: Mathlib/Analysis/Normed/Module/Span.lean

Statistics

Metric	Count
Definitions coord, toSpanNonzeroSingleton, toSpanUnitSingleton	3
Theorems coe_toSpanNonzeroSingleton_symm, coord_self, coord_toSpanNonzeroSingleton, toSpanNonzeroSingleton_apply_coe, toSpanNonzeroSingleton_coord, toSpanNonzeroSingleton_symm_apply, toSpanNonzeroSingleton_homothety, toSpanUnitSingleton_apply, toSpanSingleton_homothety	9
Total	12

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
coord 📖	CompOp	7 math math: coe_toSpanNonzeroSingleton_symm, coord_toSpanNonzeroSingleton, toSpanNonzeroSingleton_coord, coord_norm', coord_norm', coord_self, coord_norm
toSpanNonzeroSingleton 📖	CompOp	5 math math: coe_toSpanNonzeroSingleton_symm, toSpanNonzeroSingleton_symm_apply, coord_toSpanNonzeroSingleton, toSpanNonzeroSingleton_coord, toSpanNonzeroSingleton_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toSpanNonzeroSingleton_symm 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet instTopologicalSpaceSubtype Submodule.addCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Submodule.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace EquivLike.toFunLike equivLike symm toSpanNonzeroSingleton StrongDual ContinuousLinearMap.funLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule coord	—	RingHomInvPair.ids
coord_self 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Submodule ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule coord Submodule.mem_span_singleton_self AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	LinearEquiv.coord_self Field.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
coord_toSpanNonzeroSingleton 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Submodule ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule coord ContinuousLinearEquiv RingHomInvPair.ids NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace EquivLike.toFunLike equivLike toSpanNonzeroSingleton	—	symm_apply_apply RingHomInvPair.ids
toSpanNonzeroSingleton_apply_coe 📖	mathematical	—	Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpaceSubtype Submodule.addCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Submodule.module EquivLike.toFunLike equivLike toSpanNonzeroSingleton SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids
toSpanNonzeroSingleton_coord 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Submodule SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet instTopologicalSpaceSubtype Submodule.addCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Submodule.module EquivLike.toFunLike equivLike toSpanNonzeroSingleton StrongDual ContinuousLinearMap.funLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule coord	—	apply_symm_apply RingHomInvPair.ids
toSpanNonzeroSingleton_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet instTopologicalSpaceSubtype Submodule.addCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Submodule.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace EquivLike.toFunLike equivLike symm toSpanNonzeroSingleton LinearEquiv Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup LinearMap.range NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.toSpanSingleton NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearEquiv.instEquivLike LinearEquiv.symm LinearEquiv.ofInjective LinearEquiv.ofEq	—	RingHomInvPair.ids

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSpanNonzeroSingleton_homothety 📖	mathematical	—	Norm.norm Submodule Ring.toSemiring NormedRing.toRing NormedDivisionRing.toNormedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet SeminormedAddCommGroup.toNorm Submodule.seminormedAddCommGroup DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submodule.addCommMonoid Semiring.toModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toSpanNonzeroSingleton DivisionRing.isDomain NormedDivisionRing.toDivisionRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction Real Real.instMul NormedDivisionRing.toNorm	—	LinearMap.toSpanSingleton_homothety

LinearIsometryEquiv

Definitions

Name	Category	Theorems
toSpanUnitSingleton 📖	CompOp	1 math math: toSpanUnitSingleton_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSpanUnitSingleton_apply 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm Real Real.instOne	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing Submodule.seminormedAddCommGroup NormedRing.toRing Semiring.toModule Submodule.module EquivLike.toFunLike instEquivLike toSpanUnitSingleton SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSpanSingleton_homothety 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Semiring.toModule instFunLike toSpanSingleton Real Real.instMul NormedDivisionRing.toNorm	—	mul_comm norm_smul

---

← Back to Index