Documentation Verification Report

UniformRing

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

Statistics

Metric	Count
Definitions `extendRingHom`, `algebra`, `algebra'`, `coeRingHom`, `commRing`, `extensionHom`, `mapRingEquiv`, `mapRingHom`, `mul`, `one`, `commRing`, `sepQuotHomeomorphRingQuot`, `sepQuotRingEquivRingQuot`	13
Theorems `algebraMap_def`, `coe_eq_one_iff`, `coe_mapRingHom`, `coe_mul`, `coe_one`, `continuous_coeRingHom`, `extensionHom_coe`, `instContinuousMul`, `mapRingEquiv_apply`, `mapRingEquiv_symm_apply`, `mapRingHom_apply`, `mapRingHom_coe`, `mapRingHom_comp`, `mapRingHom_id`, `map_smul_eq_mul_coe`, `topologicalRing`, `inseparableSetoid_ring`, `topologicalRing`	18
Total	31

IsDenseInducing

Definitions

Name	Category	Theorems
`extendRingHom` 📖	CompOp	—

UniformSpace

Definitions

Name	Category	Theorems
`commRing` 📖	CompOp	1 math math: `topologicalRing`
`sepQuotHomeomorphRingQuot` 📖	CompOp	—
`sepQuotRingEquivRingQuot` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inseparableSetoid_ring` 📖	mathematical	—	`inseparableSetoid` `Submodule.quotientRel` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Ideal.closure` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Setoid.ext` `addGroup_inseparable_iff` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing` `Submodule.quotientRel_def`
`topologicalRing` 📖	mathematical	—	`IsTopologicalRing` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing`	—	`Topology.IsInducing.continuousAdd` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `topologicalRing_quotient` `Homeomorph.isInducing` `Topology.IsInducing.continuousMul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Topology.IsInducing.continuousNeg` `IsSemitopologicalRing.toContinuousNeg` `map_neg`

UniformSpace.Completion

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	1 math math: `algebraMap_def`
`algebra'` 📖	CompOp	1 math math: `PadicComplex.coe_eq`
`coeRingHom` 📖	CompOp	1 math math: `continuous_coeRingHom`
`commRing` 📖	CompOp	16 math math: `IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `NumberField.HeightOneSpectrum.rankOne_hom'_def`, `IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower'`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers`, `IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply`, `IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers`, `NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `LaurentSeries.powerSeries_ext_subring`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one`, `instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `PadicComplexInt.integers`
`extensionHom` 📖	CompOp	1 math math: `extensionHom_coe`
`mapRingEquiv` 📖	CompOp	2 math math: `mapRingEquiv_apply`, `mapRingEquiv_symm_apply`
`mapRingHom` 📖	CompOp	5 math math: `mapRingHom_id`, `mapRingHom_apply`, `mapRingHom_coe`, `coe_mapRingHom`, `mapRingHom_comp`
`mul` 📖	CompOp	17 math math: `mul_hatInv_cancel`, `LaurentSeries.LaurentSeriesRingEquiv_def`, `map_smul_eq_mul_coe`, `instContinuousMul`, `LaurentSeries.coe_X_compare`, `LaurentSeries.exists_powerSeries_of_memIntegers`, `LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring`, `Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `coe_mul`, `Padic.coe_withValRingEquiv`, `mapRingEquiv_apply`, `Padic.coe_withValRingEquiv_symm`, `LaurentSeries.ratfuncAdicComplRingEquiv_apply`, `mapRingEquiv_symm_apply`, `LaurentSeries.mem_integers_of_powerSeries`, `IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers`
`one` 📖	CompOp	3 math math: `mul_hatInv_cancel`, `coe_eq_one_iff`, `coe_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_def` 📖	mathematical	—	`DFunLike.coe` `RingHom` `UniformSpace.Completion` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `algebraMap` `algebra` `coe'`	—	—
`coe_eq_one_iff` 📖	mathematical	—	`coe'` `UniformSpace.Completion` `one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`coe_mapRingHom` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`DFunLike.coe` `RingHom` `UniformSpace.Completion` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `mapRingHom` `map`	—	—
`coe_mul` 📖	mathematical	—	`coe'` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `UniformSpace.Completion` `mul`	—	`IsDenseInducing.prodMap` `isDenseInducing_coe` `IsDenseInducing.extend_eq` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `t0Space` `UniformSpace.to_regularSpace` `Continuous.comp` `continuous_coe` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring`
`coe_one` 📖	mathematical	—	`coe'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `UniformSpace.Completion` `one`	—	—
`continuous_coeRingHom` 📖	mathematical	—	`Continuous` `UniformSpace.Completion` `UniformSpace.toTopologicalSpace` `uniformSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `coeRingHom`	—	`continuous_coe`
`extensionHom_coe` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`DFunLike.coe` `RingHom` `UniformSpace.Completion` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `extensionHom` `coe'`	—	`extension_coe` `uniformContinuous_addMonoidHom_of_continuous` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`instContinuousMul` 📖	mathematical	—	`ContinuousMul` `UniformSpace.Completion` `UniformSpace.toTopologicalSpace` `uniformSpace` `mul`	—	`Continuous.comp` `continuous_coe` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `isDenseInducing_coe` `IsDenseInducing.extend_Z_bilin` `IsUniformAddGroup.to_topologicalAddGroup` `isUniformAddGroup` `t0Space` `completeSpace`
`mapRingEquiv_apply` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm`	`DFunLike.coe` `RingEquiv` `UniformSpace.Completion` `mul` `instAddCompletion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mapRingEquiv` `map` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	—
`mapRingEquiv_symm_apply` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm`	`DFunLike.coe` `RingEquiv` `UniformSpace.Completion` `mul` `instAddCompletion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `mapRingEquiv` `map` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	—
`mapRingHom_apply` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`DFunLike.coe` `RingHom` `UniformSpace.Completion` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `mapRingHom` `map`	—	—
`mapRingHom_coe` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`DFunLike.coe` `RingHom` `UniformSpace.Completion` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `mapRingHom` `coe'`	—	`mapRingHom_apply` `map_coe` `uniformContinuous_addMonoidHom_of_continuous` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`mapRingHom_comp` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`RingHom.comp` `UniformSpace.Completion` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `mapRingHom` `Continuous.comp` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`DFunLike.ext'` `Continuous.comp` `map_comp` `uniformContinuous_addMonoidHom_of_continuous` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`mapRingHom_id` 📖	mathematical	—	`mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `continuous_id` `UniformSpace.toTopologicalSpace` `UniformSpace.Completion` `ring`	—	`continuous_id` `map_id`
`map_smul_eq_mul_coe` 📖	mathematical	—	`map` `Algebra.toSMul` `Ring.toSemiring` `UniformSpace.Completion` `mul` `coe'` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`induction_on` `isClosed_eq` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `t0Space` `IsTopologicalAddGroup.regularSpace` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing` `topologicalRing` `continuous_map` `continuous_const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `map_coe` `UniformContinuousConstSMul.uniformContinuous_const_smul` `Algebra.smul_def` `coe_mul`
`topologicalRing` 📖	mathematical	—	`IsTopologicalRing` `UniformSpace.Completion` `UniformSpace.toTopologicalSpace` `uniformSpace` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring`	—	`continuous_add` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `isUniformAddGroup` `continuous_mul` `instContinuousMul` `IsTopologicalAddGroup.toContinuousNeg`

---

← Back to Index