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`	10
Theorems `adic_basis`, `adic_module_basis`, `hasBasis_nhds_adic`, `hasBasis_nhds_zero_adic`, `nonarchimedean`, `hasBasis_nhds`, `hasBasis_nhds_zero`, `instIsUniformAddGroup`, `instNonarchimedeanRing`, `isAdic_iff`, `is_bot_adic_iff`, `is_ideal_adic_pow`	12
Total	22

Ideal

Definitions

Name	Category	Theorems
`adicModuleTopology` 📖	CompOp	—
`adicTopology` 📖	CompOp	3 math math: `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`
`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.toNatPow` `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.toNatPow` `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	1 math math: `instIsUniformAddGroup`
`topologicalSpaceModule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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`

(root)

Definitions

Name	Category	Theorems
`IsAdic` 📖	MathDef	2 math math: `is_bot_adic_iff`, `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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `pow_one` `mem_of_mem_nhds`
`is_ideal_adic_pow` 📖	mathematical	`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