Documentation Verification Report

Basic

📁 Source: Mathlib/NumberTheory/LocalField/Basic.lean

Statistics

Metric	Count
Definitions `IsNonarchimedeanLocalField`, `valueGroupWithZeroIsoInt`	2
Theorems `instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation`, `instCompatibleValueGroupWithZeroV`, `instCompleteSpace`, `instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation`, `instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation`, `instIsDiscrete`, `instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation`, `instIsRankLeOne`, `instIsTopologicalDivisionRing`, `isCompact_closedBall`, `toIsNontrivial`, `toIsValuativeTopology`, `toLocallyCompactSpace`	13
Total	15

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
`valueGroupWithZeroIsoInt` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation` 📖	mathematical	—	`CompactSpace` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `ValuativeRel.ValueGroupWithZero` `ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero` `ValuativeRel.valuation` `instTopologicalSpaceSubtype`	—	`isCompact_iff_compactSpace` `isCompact_closedBall`
`instCompatibleValueGroupWithZeroV` 📖	mathematical	—	`Valuation.Compatible` `ValuativeRel.ValueGroupWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero` `Valued.v` `CommRing.toRing` `IsValuativeTopology.instValuedValueGroupWithZeroOfIsUniformAddGroup`	—	—
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace`	—	`toIsValuativeTopology` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `ValuativeRel.IsRankLeOne.nonempty` `instIsRankLeOne` `StrictMono.comp` `ValuativeRel.RankLeOneStruct.strictMono` `MonoidWithZeroHom.ValueGroup₀.embedding_strictMono` `ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible` `toIsNontrivial` `instCompatibleValueGroupWithZeroV` `ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `toLocallyCompactSpace` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField`
`instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation` 📖	mathematical	—	`CompleteSpace` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `ValuativeRel.ValueGroupWithZero` `ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero` `ValuativeRel.valuation` `instUniformSpaceSubtype`	—	`toIsValuativeTopology` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `ValuativeRel.IsRankLeOne.nonempty` `instIsRankLeOne` `StrictMono.comp` `ValuativeRel.RankLeOneStruct.strictMono` `MonoidWithZeroHom.ValueGroup₀.embedding_strictMono` `ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible` `toIsNontrivial` `instCompatibleValueGroupWithZeroV`
`instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation` 📖	mathematical	—	`Finite` `IsLocalRing.ResidueField` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `ValuativeRel.ValueGroupWithZero` `ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero` `ValuativeRel.valuation` `Subring.toCommRing` `IsDiscreteValuationRing.toIsLocalRing` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Field.toSemifield` `instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation`	—	`IsValuativeTopology.instIsTopologicalAddGroup` `toIsValuativeTopology` `isUniformAddGroup_of_addCommGroup` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `ValuativeRel.IsRankLeOne.nonempty` `instIsRankLeOne` `StrictMono.comp` `ValuativeRel.RankLeOneStruct.strictMono` `MonoidWithZeroHom.ValueGroup₀.embedding_strictMono` `ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible` `toIsNontrivial` `instCompatibleValueGroupWithZeroV`
`instIsDiscrete` 📖	mathematical	—	`ValuativeRel.IsDiscrete` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`ValuativeRel.nonempty_orderIso_withZeroMul_int_iff`
`instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation` 📖	mathematical	—	`IsDiscreteValuationRing` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `ValuativeRel.ValueGroupWithZero` `ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero` `ValuativeRel.valuation` `Subring.toCommRing` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Field.toSemifield`	—	`Valued.integer.isDiscreteValuationRing_of_compactSpace` `IsValuativeTopology.instIsTopologicalAddGroup` `toIsValuativeTopology` `isUniformAddGroup_of_addCommGroup` `ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible` `toIsNontrivial` `instCompatibleValueGroupWithZeroV`
`instIsRankLeOne` 📖	mathematical	—	`ValuativeRel.IsRankLeOne` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`ValuativeRel.isRankLeOne_iff_mulArchimedean` `MulArchimedean.comap` `WithZero.instMulArchimedean` `Multiplicative.instMulArchimedean` `instArchimedeanInt` `OrderMonoidIso.strictMono`
`instIsTopologicalDivisionRing` 📖	mathematical	—	`IsTopologicalDivisionRing` `Field.toDivisionRing`	—	`Valued.isTopologicalDivisionRing` `IsValuativeTopology.instIsTopologicalAddGroup` `toIsValuativeTopology` `isUniformAddGroup_of_addCommGroup`
`isCompact_closedBall` 📖	mathematical	—	`IsCompact` `setOf` `ValuativeRel.ValueGroupWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ValuativeRel.instLEValueGroupWithZero` `DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero` `CommRing.toRing` `Valuation.instFunLike` `ValuativeRel.valuation`	—	`ValuativeRel.valuation_surjective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `GroupWithZero.toNontrivial` `LocallyCompactSpace.local_compact_nhds` `toLocallyCompactSpace` `Filter.univ_mem` `Filter.HasBasis.mem_iff` `IsValuativeTopology.hasBasis_nhds_zero'` `toIsValuativeTopology` `Valuation.IsNontrivial.exists_lt_one` `ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible` `toIsNontrivial` `ValuativeRel.instCompatibleValueGroupWithZeroValuation` `lt_or_ge` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `pow_two` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuativeRel.instIsOrderedMonoidValueGroupWithZero` `LE.le.trans_lt` `map_pow` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `HasSubset.Subset.trans` `Set.instIsTransSubset` `LT.lt.trans_le` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_le_iff` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `instIsTopologicalDivisionRing` `IsValuativeTopology.instIsTopologicalAddGroup` `isUniformAddGroup_of_addCommGroup` `Set.ext` `inv_div` `map_div₀` `div_mul_eq_mul_div` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `instMulPosStrictMonoWithZeroOfMulRightStrictMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `MulMemClass.isRightCancelMul` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `instIsRightCancelMulOfMulRightReflectLE` `contravariant_swap_mul_of_contravariant_mul` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `Units.isOrderedMonoid` `contravariant_lt_of_covariant_le` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul` `Subgroup.toIsOrderedMonoid` `WithZero.instNontrivial` `One.instNonempty` `PosMulStrictMono.toPosMulMono` `Equiv.image_eq_preimage_symm` `IsCompact.image` `IsCompact.of_isClosed_subset` `Valued.isClosed_closedBall` `Homeomorph.continuous`
`toIsNontrivial` 📖	mathematical	—	`ValuativeRel.IsNontrivial` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`toIsValuativeTopology` 📖	mathematical	—	`IsValuativeTopology` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`toLocallyCompactSpace` 📖	mathematical	—	`LocallyCompactSpace`	—	—

(root)

Definitions

Name	Category	Theorems
`IsNonarchimedeanLocalField` 📖	CompData	—

---

← Back to Index