Lemmas

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

Statistics

Metric	Count
Definitions RCLike_instance	1
Theorems properSpace_submodule, proper_rclike, rclike_to_real, aeval_conj, aeval_ofReal, ofReal_eval, conjCLE_norm, finrank_le_two, ofRealCLM_norm, rank_le_two, reCLM_norm, span_one_I, convex_RCLike_iff_convex_real	13
Total	14

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
proper_rclike 📖	mathematical	—	ProperSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	trans Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace rclike_to_real proper_real
rclike_to_real 📖	mathematical	—	FiniteDimensional Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing RCLike.toNormedAlgebra	—	Finset.coe_insert Finset.coe_singleton RCLike.span_one_I

FiniteDimensional.RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
properSpace_submodule 📖	mathematical	—	ProperSpace Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace	—	FiniteDimensional.proper_rclike IsScalarTower.left

LibraryNote

Definitions

Name	Category	Theorems
RCLike_instance 📖	CompOp	—

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_conj 📖	mathematical	—	DFunLike.coe AlgHom Real Polynomial CommSemiring.toSemiring Real.instCommSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring Semifield.toCommSemiring RingHom.instFunLike starRingEnd RCLike.toStarRing	—	aeval_algHom_apply AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
aeval_ofReal 📖	mathematical	—	DFunLike.coe AlgHom Real Polynomial CommSemiring.toSemiring Real.instCommSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra AlgHom.funLike aeval RCLike.ofReal eval Real.semiring	—	aeval_algHom_apply AlgHom.algHomClass
ofReal_eval 📖	mathematical	—	RCLike.ofReal eval Real Real.semiring DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Real.instCommSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra AlgHom.funLike aeval	—	aeval_algebraMap_apply_eq_algebraMap_eval

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjCLE_norm 📖	mathematical	—	Norm.norm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace toNormedAlgebra ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids conjCLE Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap IsLocalRing.toNontrivial Field.instIsLocalRing RingHomIsometric.ids RingHomInvPair.ids
finrank_le_two 📖	mathematical	—	Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace toNormedAlgebra	—	Module.finrank_le_of_rank_le rank_le_two
ofRealCLM_norm 📖	mathematical	—	Norm.norm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedAlgebra.toNormedSpace toNormedAlgebra ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField ofRealCLM Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap Real.instNontrivial RingHomIsometric.ids
rank_le_two 📖	mathematical	—	Cardinal Cardinal.instLE Module.rank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace toNormedAlgebra instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat span_one_I rank_top rank_span_finset_le commRing_strongRankCondition Real.instNontrivial Finset.coe_pair Nat.cast_one Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero Finset.card_le_two
reCLM_norm 📖	mathematical	—	Norm.norm StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace toNormedAlgebra ContinuousLinearMap.hasOpNorm Real.normedCommRing DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NontriviallyNormedField.toNormedField NormedField.toNormedSpace RingHom.id Semiring.toNonAssocSemiring reCLM Real.instOne	—	le_antisymm LinearMap.mkContinuous_norm_le zero_le_one Real.instZeroLEOneClass one_re CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass instCStarRing IsLocalRing.toNontrivial Field.instIsLocalRing div_self NeZero.charZero_one charZero_rclike ContinuousLinearMap.ratio_le_opNorm RingHomIsometric.ids
span_one_I 📖	mathematical	—	Submodule.span Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace toNormedAlgebra Set Set.instInsert AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Set.instSingletonSet I Top.top Submodule Submodule.instTop	—	real_smul_eq_coe_mul mul_one re_add_im

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convex_RCLike_iff_convex_real 📖	mathematical	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toPartialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Real Real.semiring Real.partialOrder Real.instMonoid	—	Convex.lift RCLike.toZeroLEOneClass PosSMulMono.toSMulPosMono Real.instIsOrderedRing RCLike.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono instIsOrderedModule RCLike.toStarOrderedRing RCLike.instStarModuleReal IsScalarTower.right Algebra.to_smulCommClass convex_of_nonneg_surjective_algebraMap instFaithfulSMul_1 DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing RCLike.nonneg_iff_exists_ofReal

---

← Back to Index