Documentation Verification Report

UniformField

📁 Source: Mathlib/Topology/Algebra/UniformField.lean

Statistics

Metric	Count
Definitions `CompletableTopField`, `hatInv`, `instField`, `instInvCompletion`	4
Theorems `nice`, `toT0Space`, `completableTopField`, `completableTopField`, `coe_inv`, `continuous_hatInv`, `hatInv_extends`, `instIsTopologicalDivisionRing`, `instNontrivialOfT0Space`, `mul_hatInv_cancel`, `completableTopField_of_complete`	11
Total	15

CompletableTopField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nice` 📖	mathematical	`Cauchy` `Filter` `Filter.instInf` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Bot.bot` `Filter.instBot`	`Filter.map` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	—
`toT0Space` 📖	mathematical	—	`T0Space` `UniformSpace.toTopologicalSpace`	—	—

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completableTopField` 📖	mathematical	`IsUniformInducing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike`	`CompletableTopField`	—	`cauchy_map_iff` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Filter.map_comm` `CompletableTopField.nice` `Filter.push_pull'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Topology.IsInducing.nhds_eq_comap` `isInducing` `Filter.map_bot`

Subfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completableTopField` 📖	mathematical	—	`CompletableTopField` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `toField` `instUniformSpaceSubtype`	—	`Subtype.t0Space` `CompletableTopField.toT0Space` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_subtype_val` `IsUniformInducing.cauchy_map_iff` `Filter.map_comm` `CompletableTopField.nice` `Filter.push_pull'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Topology.IsInducing.nhds_eq_comap` `IsUniformInducing.isInducing` `Filter.map_bot`

UniformSpace.Completion

Definitions

Name	Category	Theorems
`hatInv` 📖	CompOp	3 math math: `mul_hatInv_cancel`, `continuous_hatInv`, `hatInv_extends`
`instField` 📖	CompOp	42 math math: `NumberField.FinitePlace.mk_apply`, `PadicComplex.coe_eq`, `IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `NumberField.FinitePlace.norm_def'`, `IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers`, `NumberField.FinitePlace.embedding_apply`, `PadicComplex.norm_def`, `IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower'`, `NumberField.FinitePlace.norm_embedding_eq`, `LaurentSeries.algebraMap_C_mem_adicCompletionIntegers`, `IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply`, `IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers`, `IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `NumberField.FinitePlace.norm_lt_one_iff_mem`, `IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `NumberField.FinitePlace.norm_def_int`, `instIsTopologicalDivisionRing`, `LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation`, `IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers`, `LaurentSeries.powerSeries_ext_subring`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `NumberField.FinitePlace.norm_eq_one_iff_notMem`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one`, `instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one`, `IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm`, `NumberField.FinitePlace.norm_le_one`, `LaurentSeries.mem_integers_of_powerSeries`, `IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion`, `IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers`, `PadicComplexInt.integers`, `NumberField.FinitePlace.norm_def`, `IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers`
`instInvCompletion` 📖	CompOp	1 math math: `coe_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inv` 📖	mathematical	—	`UniformSpace.Completion` `instInvCompletion` `coe'` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	`inv_zero` `Nat.cast_zero` `IsDenseEmbedding.injective` `isDenseEmbedding_coe` `CompletableTopField.toT0Space` `hatInv_extends`
`continuous_hatInv` 📖	mathematical	—	`ContinuousAt` `UniformSpace.Completion` `UniformSpace.toTopologicalSpace` `uniformSpace` `hatInv`	—	`IsDenseInducing.continuousAt_extend` `instT3Space` `t0Space` `UniformSpace.to_regularSpace` `isDenseInducing_coe` `Filter.mem_of_superset` `compl_singleton_mem_nhds` `T2Space.t1Space` `T25Space.t2Space` `T3Space.t25Space` `CompleteSpace.complete` `completeSpace` `Filter.map_map` `Cauchy.map` `CompletableTopField.nice` `Cauchy.comap` `cauchy_nhds` `comap_coe_eq_uniformity` `le_refl` `IsDenseInducing.comap_nhds_neBot` `Set.mem_compl_singleton_iff` `eq_of_nhds_neBot` `Filter.neBot_iff` `IsDenseInducing.nhds_eq_comap` `Filter.comap_inf` `Nat.cast_zero` `Filter.comap_bot` `uniformContinuous_coe`
`hatInv_extends` 📖	mathematical	—	`hatInv` `coe'` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	`IsDenseInducing.extend_eq_at` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `t0Space` `UniformSpace.to_regularSpace` `isDenseInducing_coe` `ContinuousAt.comp` `Continuous.continuousAt` `continuous_coe` `ContinuousInv₀.continuousAt_inv₀` `IsTopologicalDivisionRing.toContinuousInv₀`
`instIsTopologicalDivisionRing` 📖	mathematical	—	`IsTopologicalDivisionRing` `UniformSpace.Completion` `Field.toDivisionRing` `instField` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`topologicalRing` `Filter.mem_of_superset` `compl_singleton_mem_nhds` `T2Space.t1Space` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `t0Space` `IsTopologicalAddGroup.regularSpace` `IsTopologicalRing.to_topologicalAddGroup` `IsTopologicalDivisionRing.toIsTopologicalRing` `Set.mem_compl_singleton_iff` `ContinuousAt.congr` `continuous_hatInv`
`instNontrivialOfT0Space` 📖	mathematical	—	`Nontrivial` `UniformSpace.Completion`	—	`Function.Injective.nontrivial` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `IsUniformEmbedding.injective` `isUniformEmbedding_coe`
`mul_hatInv_cancel` 📖	mathematical	—	`UniformSpace.Completion` `mul` `DivisionRing.toRing` `Field.toDivisionRing` `hatInv` `one`	—	`ContinuousAt.fun_mul` `instContinuousMul` `IsTopologicalDivisionRing.toIsTopologicalRing` `continuousAt_id'` `continuous_hatInv` `IsDenseInducing.dense` `isDenseInducing_coe` `mem_closure_of_mem_closure_union` `Set.image_union` `Set.union_compl_self` `Set.image_univ` `Set.image_singleton` `compl_singleton_mem_nhds` `T2Space.t1Space` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `t0Space` `IsTopologicalAddGroup.regularSpace` `IsTopologicalRing.to_topologicalAddGroup` `topologicalRing` `mem_closure_image` `Set.image_image` `Set.mem_singleton_iff` `hatInv_extends` `Set.mem_compl_singleton_iff` `coe_mul` `mul_inv_cancel₀` `coe_one` `closure_mono` `closure_singleton`

(root)

Definitions

Name	Category	Theorems
`CompletableTopField` 📖	CompData	5 math math: `IsUniformInducing.completableTopField`, `NormedField.instCompletableTopField`, `Valued.completable`, `Subfield.completableTopField`, `completableTopField_of_complete`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completableTopField_of_complete` 📖	mathematical	—	`CompletableTopField`	—	`CompleteSpace.complete` `Filter.NeBot.ne` `inf_eq_right` `Filter.Tendsto.cauchy_map` `Filter.map_mono` `ContinuousInv₀.continuousAt_inv₀` `IsTopologicalDivisionRing.toContinuousInv₀`

---

← Back to Index