LocallyCompact

📁 Source: Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

Statistics

Metric	Count
Definitions	0
Theorems maximalIdeal_eq_closedBall, maximalIdeal_pow_eq_closedBall_pow, v_eq_valuation, isNontrivial_iff_not_a_field, coe_span_singleton_eq_closedBall, compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, exists_nnnorm_lt_one, exists_norm_coe_lt_one, exists_norm_lt_one, finite_quotient_maximalIdeal_pow_of_finite_residueField, isDiscreteValuationRing_of_compactSpace, isPrincipalIdealRing_of_compactSpace, isUnit_iff_norm_eq_one, locallyFiniteOrder_units_mrange_of_isCompact_integer, mem_iff, mulArchimedean_mrange_of_isCompact_integer, norm_coe_unit, norm_irreducible_lt_one, norm_irreducible_pos, norm_le_one, norm_unit, properSpace_iff_compactSpace_integer, properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, totallyBounded_iff_finite_residueField	24
Total	24

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximalIdeal_eq_closedBall 📖	mathematical	Irreducible Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	SetLike.coe Ideal Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Valued.maximalIdeal Metric.closedBall Subtype.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SubringClass.addSubgroupClass Norm.norm NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing	—	Subring.instIsDomainSubtypeMem instIsDomain SubringClass.toSubsemiringClass Subring.instSubringClass AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass SubringClass.addSubgroupClass IsDiscreteValuationRing.toIsLocalRing maximalIdeal_eq_setOf_le_v_coe dist_zero_right
maximalIdeal_pow_eq_closedBall_pow 📖	mathematical	Irreducible Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	SetLike.coe Ideal Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Valued.maximalIdeal Metric.closedBall Subtype.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SubringClass.addSubgroupClass Real Monoid.toPow Real.instMonoid Norm.norm NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing	—	Subring.instIsDomainSubtypeMem instIsDomain SubringClass.toSubsemiringClass Subring.instSubringClass IsScalarTower.right AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass SubringClass.addSubgroupClass IsDiscreteValuationRing.toIsLocalRing maximalIdeal_pow_eq_setOf_le_v_coe_pow dist_zero_right

NormedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
v_eq_valuation 📖	mathematical	—	DFunLike.coe Valuation NNReal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero NormedRing.toRing NormedCommRing.toNormedRing toNormedCommRing NontriviallyNormedField.toNormedField Valuation.instFunLike Valued.v toValued valuation	—	—

Valuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNontrivial_iff_not_a_field 📖	mathematical	—	IsNontrivial DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	SubringClass.toSubsemiringClass Subring.instSubringClass ValuationRing.isLocalRing Subring.instNontrivialSubtypeMem EuclideanDomain.toNontrivial ValuationRing.toPreValuationRing Subring.instIsDomainSubtypeMem instIsDomain ValuationRing.instValuationRingInteger isNontrivial_iff_exists_lt_one instIsConcreteLE Iff.not_right IsLocalRing.notMem_maximalIdeal LT.lt.le AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass SubringClass.addSubgroupClass

Valued.integer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_span_singleton_eq_closedBall 📖	mathematical	—	SetLike.coe Ideal Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet Metric.closedBall Subtype.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SubringClass.addSubgroupClass Norm.norm NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing	—	SubringClass.toSubsemiringClass Subring.instSubringClass AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass SubringClass.addSubgroupClass Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe dist_zero_right
compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField 📖	mathematical	—	CompactSpace Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing CompleteSpace instUniformSpaceSubtype IsDiscreteValuationRing Subring.toCommRing Subring.instIsDomainSubtypeMem CommRing.toRing instIsDomain Field.toSemifield Finite Valued.ResidueField	—	Subring.instIsDomainSubtypeMem instIsDomain isDiscreteValuationRing_of_compactSpace Valuation.RankOne.instIsNontrivial complete_of_compact totallyBounded_iff_finite_residueField isCompact_iff_totallyBounded_isComplete isCompact_univ_iff completeSpace_iff_isComplete_univ
exists_nnnorm_lt_one 📖	mathematical	—	Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SubringClass.toSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Subring.instSubringClass NNReal.instOne	—	exists_norm_coe_lt_one
exists_norm_coe_lt_one 📖	mathematical	—	Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued Real Real.instLT Real.instZero Norm.norm NormedField.toNorm Real.instOne	—	NormedField.exists_norm_lt_one LT.lt.le
exists_norm_lt_one 📖	mathematical	—	Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued Real Real.instLT Real.instZero Norm.norm NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Subring.instSubringClass Real.instOne	—	exists_norm_coe_lt_one
finite_quotient_maximalIdeal_pow_of_finite_residueField 📖	mathematical	—	Finite HasQuotient.Quotient Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Ideal.instHasQuotient_1 Subring.toCommRing Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id Valued.maximalIdeal	—	Subring.instIsDomainSubtypeMem instIsDomain SubringClass.toSubsemiringClass Subring.instSubringClass IsScalarTower.right pow_zero Ideal.one_eq_top Finite.of_fintype Ideal.pow_le_pow_right IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Ideal.instIsTwoSided_1 Finite.of_equiv Submodule.isScalarTower' IsPrincipalIdealRing.principal IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.not_a_field Finite.of_ideal_quotient
isDiscreteValuationRing_of_compactSpace 📖	mathematical	—	IsDiscreteValuationRing Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer Subring.toCommRing Subring.instIsDomainSubtypeMem CommRing.toRing instIsDomain Field.toSemifield	—	SubringClass.toSubsemiringClass Subring.instSubringClass isPrincipalIdealRing_of_compactSpace Subring.instIsDomainSubtypeMem instIsDomain ValuationRing.isLocalRing Subring.instNontrivialSubtypeMem EuclideanDomain.toNontrivial ValuationRing.toPreValuationRing ValuationRing.instValuationRingInteger Valuation.isNontrivial_iff_not_a_field
isPrincipalIdealRing_of_compactSpace 📖	mathematical	—	IsPrincipalIdealRing Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	—	Valuation.integer.integers isCompact_iff_compactSpace MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass SubringClass.toSubsemiringClass Subring.instSubringClass locallyFiniteOrder_units_mrange_of_isCompact_integer mulArchimedean_mrange_of_isCompact_integer Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange not_subsingleton instNontrivialUnitsOfDenselyOrdered LocallyFiniteOrder.denselyOrdered_iff_subsingleton instDenselyOrderedUnits
isUnit_iff_norm_eq_one 📖	mathematical	—	IsUnit Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Norm.norm NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Real Real.instOne	—	Valuation.Integers.isUnit_iff_valuation_eq_one Valuation.integer.integers
locallyFiniteOrder_units_mrange_of_isCompact_integer 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring.instSetLike Valued.integer	LocallyFiniteOrder Units Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero SetLike.instMembership Submonoid.instSetLike MonoidHom.mrange NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike MonoidWithZeroHomClass.toMonoidHomClass Ring.toSemiring CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valued.v Submonoid.toMonoid MonoidWithZero.toMonoid Units.instPreorder Subtype.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Subtype.prop lt_or_ge Set.Icc_eq_empty_of_lt Set.finite_empty Subtype.coe_lt_coe IsCompact.elim_finite_subcover MonoidHom.mem_mrange MonoidWithZeroHom.monoidWithZeroHomClass Valuation.restrict_le_iff Valued.isOpen_closedBall map_zero MonoidWithZeroHomClass.toZeroHomClass LT.lt.ne' Valued.isOpen_sphere LT.lt.trans' instReflLe Set.Finite.subset Subtype.coe_injective Set.Finite.dependent_image Finset.finite_toSet Eq.trans_le Set.iUnion_congr_Prop le_antisymm Subtype.coe_eta lt_trichotomy Set.Icc_self le_total Set.Icc_subset_Icc_right Set.Finite.union Set.Finite.inv le_of_eq Set.inv_Icc Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid inv_one Set.Icc_union_Icc_eq_Icc inv_inv inv_lt_inv' inv_le_one_of_one_le LT.lt.le LT.lt.trans
mem_iff 📖	mathematical	—	Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued Real Real.instLE Norm.norm NormedField.toNorm Real.instOne	—	—
mulArchimedean_mrange_of_isCompact_integer 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring.instSetLike Valued.integer	MulArchimedean Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero SetLike.instMembership Submonoid.instSetLike MonoidHom.mrange NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike MonoidWithZeroHomClass.toMonoidHomClass Ring.toSemiring CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valued.v Submonoid.toCommMonoid CommMonoidWithZero.toCommMonoid Subtype.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Units.mulArchimedean_iff locallyFiniteOrder_units_mrange_of_isCompact_integer MulArchimedean.of_locallyFiniteOrder Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid
norm_coe_unit 📖	mathematical	—	Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Real Real.instOne	—	SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.Integers.valuation_unit Valuation.integer.integers
norm_irreducible_lt_one 📖	mathematical	Irreducible Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	Real Real.instLT Norm.norm Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Subring.instSubringClass Real.instOne	—	SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.integer.v_irreducible_lt_one
norm_irreducible_pos 📖	mathematical	Irreducible Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	Real Real.instLT Real.instZero Norm.norm Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Subring.instSubringClass	—	SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.integer.v_irreducible_pos
norm_le_one 📖	mathematical	—	Real Real.instLE Norm.norm Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Subring.instSubringClass Real.instOne	—	Subring.instSubringClass mem_iff Subtype.prop
norm_unit 📖	mathematical	—	Norm.norm Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField SetLike.instMembership Subring.instSetLike Valued.integer NNReal NNReal.instLinearOrderedCommGroupWithZero NormedField.toValued NormedRing.toNorm SubringClass.toNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Subring.instSubringClass Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Real Real.instOne	—	SubringClass.toSubsemiringClass Subring.instSubringClass norm_coe_unit
properSpace_iff_compactSpace_integer 📖	mathematical	—	ProperSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Valued.toNormedField CompactSpace Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing	—	Set.image_univ Subtype.range_coe_subtype Valued.toNormedField.setOf_mem_integer_eq_closedBall ProperSpace.isCompact_closedBall IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup NonarchimedeanAddGroup.toIsTopologicalAddGroup IsUltrametricDist.nonarchimedeanAddGroup Valued.instIsUltrametricDist Metric.closedBall_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace
properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField 📖	mathematical	—	ProperSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Valued.toNormedField CompleteSpace Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing IsDiscreteValuationRing Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer Subring.toCommRing Subring.instIsDomainSubtypeMem CommRing.toRing instIsDomain Field.toSemifield Finite Valued.ResidueField	—	Subring.instIsDomainSubtypeMem instIsDomain completeSpace_iff_isComplete_univ Set.image_univ Subtype.range_coe_subtype Valued.toNormedField.setOf_mem_integer_eq_closedBall
totallyBounded_iff_finite_residueField 📖	mathematical	—	TotallyBounded Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subring.instSetLike Valued.integer instUniformSpaceSubtype Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing Set.univ Finite Valued.ResidueField	—	Subring.instIsDomainSubtypeMem instIsDomain IsDiscreteValuationRing.exists_irreducible Subring.instSubringClass Metric.finite_approx_of_totallyBounded norm_pos_iff Irreducible.ne_zero SubringClass.toSubsemiringClass Set.finite_univ_iff Set.Finite.subset Set.Finite.image Eq.ge Set.mem_univ Ideal.instIsTwoSided_1 Set.image_congr Ideal.Quotient.mk_eq_mk_iff_sub_mem Valued.maximalIdeal.eq_1 IsDiscreteValuationRing.toIsLocalRing Irreducible.maximalIdeal_eq SetLike.mem_coe Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap Valuation.integer.integers map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass dist_eq_norm LT.lt.le dist_comm Metric.totallyBounded_iff Valuation.integer.v_irreducible_lt_one exists_pow_lt_of_lt_one Real.instIsStrictOrderedRing Real.instArchimedean AddGroup.existsAddOfLE Valued.toNormedField.norm_lt_one_iff IsScalarTower.right finite_quotient_maximalIdeal_pow_of_finite_residueField Set.toFinite Finite.Set.finite_image Subtype.finite AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass SubringClass.addSubgroupClass Set.ext NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass dist_zero_right map_pow MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Ideal.univ_eq_iUnion_image_add Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow Metric.vadd_closedBall NormedAddGroup.to_isIsometricVAdd add_zero Set.iUnion_congr_Prop Set.image_univ Set.iUnion_exists Set.iUnion_iUnion_eq' HasSubset.Subset.trans Set.instIsTransSubset Metric.closedBall_subset_ball Set.subset_iUnion_of_subset le_rfl

---

← Back to Index