Documentation Verification Report

AdicTopology

📁 Source: Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean

Statistics

Metric	Count
Definitions `adicModuleTopology`, `adicTopology`, `openAddSubgroup`, `ringFilterBasis`, `IsAdic`, `WithIdeal`, `i`, `instTopologicalSpace`, `instUniformSpace`, `topologicalSpaceModule`, `uniformEquiv`	11
Theorems `adic_basis`, `adic_module_basis`, `hasBasis_nhds_adic`, `hasBasis_nhds_zero_adic`, `isLinearTopology`, `nonarchimedean`, `hasBasis_nhds`, `hasBasis_nhds_zero`, `instIsLinearTopology`, `instIsUniformAddGroup`, `instNonarchimedeanRing`, `isTopologicallyNilpotent_of_mem`, `uniformContinuous_of_map_le`, `isAdic_iff`, `is_bot_adic_iff`, `is_ideal_adic_pow`	16
Total	27

Ideal

Definitions

Name	Category	Theorems
`adicModuleTopology` 📖	CompOp	—
`adicTopology` 📖	CompOp	4 math math: `isLinearTopology`, `nonarchimedean`, `hasBasis_nhds_zero_adic`, `hasBasis_nhds_adic`
`openAddSubgroup` 📖	CompOp	—
`ringFilterBasis` 📖	CompOp	1 math math: `adic_module_basis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adic_basis` 📖	mathematical	—	`SubmodulesRingBasis` `Algebra.id` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Submodule.instSMul` `Semiring.toModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsScalarTower.right` `Submodule.instPowNat` `Top.top` `Submodule.instTop`	—	`IsScalarTower.right` `pow_le_pow_right` `le_max_left` `le_max_right` `mul_top` `instIsTwoSided_1` `Algebra.to_smulCommClass` `Submodule.smul_mem` `IsScalarTower.to_smulCommClass'` `IsScalarTower.left` `smul_top_eq_map` `Submodule.restrictScalars.congr_simp` `map_id`
`adic_module_basis` 📖	mathematical	—	`RingFilterBasis.SubmodulesBasis` `ringFilterBasis` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Top.top` `Submodule.instTop`	—	`IsScalarTower.left` `IsScalarTower.right` `le_inf_iff` `Submodule.smul_mono_left` `pow_le_pow_right` `le_max_left` `le_max_right` `mul_top` `instIsTwoSided_1` `Submodule.smul_mem_smul` `Submodule.mem_top`
`hasBasis_nhds_adic` 📖	mathematical	—	`Filter.HasBasis` `nhds` `adicTopology` `Set.image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `Filter.HasBasis.map` `hasBasis_nhds_zero_adic` `map_add_left_nhds_zero` `AddGroupFilterBasis.isTopologicalAddGroup` `SubmodulesRingBasis.toRing_subgroups_basis` `adic_basis`
`hasBasis_nhds_zero_adic` 📖	mathematical	—	`Filter.HasBasis` `nhds` `adicTopology` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `Filter.HasBasis.mem_iff` `AddGroupFilterBasis.nhds_zero_hasBasis` `mul_top` `instIsTwoSided_1`
`isLinearTopology` 📖	mathematical	—	`IsLinearTopology` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `adicTopology`	—	`IsLinearTopology.mk_of_hasBasis` `Submodule.smulMemClass` `Submodule.addSubmonoidClass` `IsScalarTower.right` `hasBasis_nhds_zero_adic`
`nonarchimedean` 📖	mathematical	—	`NonarchimedeanRing` `CommRing.toRing` `adicTopology`	—	`RingSubgroupsBasis.nonarchimedean` `IsScalarTower.right` `SubmodulesRingBasis.toRing_subgroups_basis` `adic_basis`

IsAdic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis_nhds` 📖	mathematical	`IsAdic`	`Filter.HasBasis` `nhds` `Set.image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	—	`Ideal.hasBasis_nhds_adic`
`hasBasis_nhds_zero` 📖	mathematical	`IsAdic`	`Filter.HasBasis` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	—	`Ideal.hasBasis_nhds_zero_adic`

WithIdeal

Definitions

Name	Category	Theorems
`i` 📖	CompOp	—
`instTopologicalSpace` 📖	CompOp	1 math math: `instNonarchimedeanRing`
`instUniformSpace` 📖	CompOp	4 math math: `instIsLinearTopology`, `isTopologicallyNilpotent_of_mem`, `uniformContinuous_of_map_le`, `instIsUniformAddGroup`
`topologicalSpaceModule` 📖	CompOp	—
`uniformEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLinearTopology` 📖	mathematical	—	`IsLinearTopology` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`Ideal.isLinearTopology`
`instIsUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `instUniformSpace` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`isUniformAddGroup_of_addCommGroup`
`instNonarchimedeanRing` 📖	mathematical	—	`NonarchimedeanRing` `CommRing.toRing` `instTopologicalSpace`	—	`RingSubgroupsBasis.nonarchimedean` `SubmodulesRingBasis.toRing_subgroups_basis` `Ideal.adic_basis`
`isTopologicallyNilpotent_of_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `i`	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`IsScalarTower.right` `Ideal.pow_le_pow_right` `Ideal.pow_mem_pow` `Filter.HasBasis.tendsto_right_iff` `Ideal.hasBasis_nhds_zero_adic` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`uniformContinuous_of_map_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `i`	`UniformContinuous` `instUniformSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`uniformContinuous_of_continuousAt_zero` `instIsUniformAddGroup` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `ContinuousAt.eq_1` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsScalarTower.right` `Filter.HasBasis.tendsto_iff` `Ideal.hasBasis_nhds_zero_adic` `Ideal.map_le_iff_le_comap` `Ideal.map_pow` `Ideal.pow_right_mono`

(root)

Definitions

Name	Category	Theorems
`IsAdic` 📖	MathDef	3 math math: `is_bot_adic_iff`, `is_ideal_adic_pow`, `isAdic_iff`
`WithIdeal` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAdic_iff` 📖	mathematical	—	`IsAdic` `IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Set` `Set.instHasSubset`	—	`IsScalarTower.right` `OpenAddSubgroup.isOpen'` `Filter.HasBasis.mem_iff` `Ideal.hasBasis_nhds_zero_adic` `IsTopologicalAddGroup.ext` `IsTopologicalRing.to_topologicalAddGroup` `AddGroupFilterBasis.isTopologicalAddGroup` `SubmodulesRingBasis.toRing_subgroups_basis` `Ideal.adic_basis` `Filter.ext` `mem_nhds_iff` `Ideal.zero_mem`
`is_bot_adic_iff` 📖	mathematical	—	`IsAdic` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DiscreteTopology`	—	`IsScalarTower.right` `isAdic_iff` `discreteTopology_iff_isOpen_singleton_zero` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `pow_one` `mem_of_mem_nhds`
`is_ideal_adic_pow` 📖	mathematical	`IsAdic`	`IsAdic` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `isAdic_iff` `pow_mul` `Set.Subset.trans` `Ideal.pow_le_pow_right`

---

← Back to Index