Basic

📁 Source: Mathlib/Analysis/Normed/Algebra/Basic.lean

Statistics

Metric	Count
Definitions instNontriviallyNormedFieldSubtypeMem	1
Theorems instCompactSpaceElemCharacterSpaceOfProperSpace, norm_le_norm_one	2
Total	3

IntermediateField

Definitions

Name	Category	Theorems
instNontriviallyNormedFieldSubtypeMem 📖	CompOp	—

WeakDual.CharacterSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpaceElemCharacterSpaceOfProperSpace 📖	mathematical	—	CompactSpace Set.Elem WeakDual Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing WeakDual.characterSpace instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceWeakDual	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul isCompact_iff_compactSpace RingHomInvPair.ids Algebra.to_smulCommClass RingHomIsometric.ids Set.mem_preimage mem_closedBall_zero_iff norm_le_norm_one IsCompact.of_isClosed_subset WeakDual.isCompact_closedBall isClosed NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsLocalRing.toNontrivial Field.instIsLocalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring
norm_le_norm_one 📖	mathematical	—	Real Real.instLE Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedRing.toSeminormedRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace ContinuousLinearMap.hasOpNorm NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids WeakDual Semifield.toCommSemiring IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring IsSemitopologicalSemiring.toSeparatelyContinuousMul instAddCommMonoidWeakDual ContinuousLinearMap.addCommMonoid Semiring.toModule WeakDual.instModule' Algebra.to_smulCommClass Algebra.id ContinuousLinearMap.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv WeakDual.toStrongDual Set Set.instMembership WeakDual.characterSpace NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousLinearMap.opNorm_le_bound RingHomInvPair.ids Algebra.to_smulCommClass norm_nonneg spectrum.norm_le_norm_mul_of_mem apply_mem_spectrum NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsLocalRing.toNontrivial Field.instIsLocalRing mul_comm

---

← Back to Index