Documentation Verification Report

Bases

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

Statistics

Metric	Count
Definitions `«non-Archimedean_non-instances»`, `SubmodulesBasis`, `moduleFilterBasis`, `RingSubgroupsBasis`, `openAddSubgroup`, `toRingFilterBasis`, `topology`, `SubmodulesBasis`, `openAddSubgroup`, `toModuleFilterBasis`, `topology`, `SubmodulesRingBasis`, `topology`	13
Theorems `inter`, `smul`, `submodulesBasisIsBasis`, `hasBasis_nhds`, `hasBasis_nhds_zero`, `inter`, `leftMul`, `mem_addGroupFilterBasis`, `mem_addGroupFilterBasis_iff`, `mul`, `nonarchimedean`, `of_comm`, `rightMul`, `inter`, `nonarchimedean`, `smul`, `inter`, `leftMul`, `mul`, `toRing_subgroups_basis`, `toSubmodulesBasis`	21
Total	34

LibraryNote

Definitions

Name	Category	Theorems
`«non-Archimedean_non-instances»` 📖	CompOp	—

RingFilterBasis

Definitions

Name	Category	Theorems
`SubmodulesBasis` 📖	CompData	1 math math: `Ideal.adic_module_basis`
`moduleFilterBasis` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`submodulesBasisIsBasis` 📖	mathematical	`SubmodulesBasis`	`SubmodulesBasis` `topology` `CommRing.toRing`	—	`SubmodulesBasis.inter` `SubmodulesBasis.smul` `Filter.mem_of_superset` `AddGroupFilterBasis.mem_nhds_zero`

RingFilterBasis.SubmodulesBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter` 📖	mathematical	`RingFilterBasis.SubmodulesBasis`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instMin`	—	—
`smul` 📖	mathematical	`RingFilterBasis.SubmodulesBasis`	`Set` `RingFilterBasis` `CommRing.toRing` `RingFilterBasis.instMembershipSet` `Set.instHasSubset` `Set.preimage` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Submodule` `Submodule.setLike`	—	—

RingSubgroupsBasis

Definitions

Name	Category	Theorems
`openAddSubgroup` 📖	CompOp	—
`toRingFilterBasis` 📖	CompOp	3 math math: `Valued.toUniformSpace_eq`, `mem_addGroupFilterBasis`, `mem_addGroupFilterBasis_iff`
`topology` 📖	CompOp	4 math math: `Valued.toUniformSpace_eq`, `hasBasis_nhds_zero`, `hasBasis_nhds`, `nonarchimedean`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis_nhds` 📖	mathematical	`RingSubgroupsBasis`	`Filter.HasBasis` `nhds` `topology` `setOf` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SetLike.instMembership` `AddSubgroup.instSetLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Filter.HasBasis.mem_iff` `AddGroupFilterBasis.nhds_hasBasis` `Set.image_add_left` `neg_add_eq_sub` `Set.ext` `Set.image_subset_iff` `add_sub_cancel_left`
`hasBasis_nhds_zero` 📖	mathematical	`RingSubgroupsBasis`	`Filter.HasBasis` `nhds` `topology` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.coe` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instSetLike`	—	`Filter.HasBasis.mem_iff` `AddGroupFilterBasis.nhds_zero_hasBasis`
`inter` 📖	mathematical	`RingSubgroupsBasis`	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.instMin`	—	—
`leftMul` 📖	mathematical	`RingSubgroupsBasis`	`Set` `Set.instHasSubset` `SetLike.coe` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instSetLike` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`mem_addGroupFilterBasis` 📖	mathematical	`RingSubgroupsBasis`	`Set` `AddGroupFilterBasis` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddGroupFilterBasis.instMembershipSet` `RingFilterBasis.toAddGroupFilterBasis` `toRingFilterBasis` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	—	—
`mem_addGroupFilterBasis_iff` 📖	mathematical	`RingSubgroupsBasis`	`Set` `AddGroupFilterBasis` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddGroupFilterBasis.instMembershipSet` `RingFilterBasis.toAddGroupFilterBasis` `toRingFilterBasis` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike`	—	—
`mul` 📖	mathematical	`RingSubgroupsBasis`	`Set` `Set.instHasSubset` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.coe` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instSetLike`	—	—
`nonarchimedean` 📖	mathematical	`RingSubgroupsBasis`	`NonarchimedeanRing` `topology`	—	`RingFilterBasis.isTopologicalRing` `Filter.HasBasis.mem_iff` `hasBasis_nhds_zero`
`of_comm` 📖	mathematical	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.instMin` `Set` `Set.instHasSubset` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe` `AddSubgroup.instSetLike` `Set.preimage`	`RingSubgroupsBasis`	—	`mul_comm`
`rightMul` 📖	mathematical	`RingSubgroupsBasis`	`Set` `Set.instHasSubset` `SetLike.coe` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instSetLike` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—

SubmodulesBasis

Definitions

Name	Category	Theorems
`openAddSubgroup` 📖	CompOp	—
`toModuleFilterBasis` 📖	CompOp	—
`topology` 📖	CompOp	1 math math: `nonarchimedean`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter` 📖	mathematical	`SubmodulesBasis`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instMin`	—	—
`nonarchimedean` 📖	mathematical	`SubmodulesBasis`	`NonarchimedeanAddGroup` `AddCommGroup.toAddGroup` `topology`	—	`AddGroupFilterBasis.isTopologicalAddGroup` `Filter.HasBasis.mem_iff` `AddGroupFilterBasis.nhds_zero_hasBasis`
`smul` 📖	mathematical	`SubmodulesBasis`	`Filter.Eventually` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—

SubmodulesRingBasis

Definitions

Name	Category	Theorems
`topology` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter` 📖	mathematical	`SubmodulesRingBasis`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instMin`	—	—
`leftMul` 📖	mathematical	`SubmodulesRingBasis`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right`	—	—
`mul` 📖	mathematical	`SubmodulesRingBasis`	`Set` `Set.instHasSubset` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Submodule.setLike`	—	—
`toRing_subgroups_basis` 📖	mathematical	`SubmodulesRingBasis`	`RingSubgroupsBasis` `CommRing.toRing` `Submodule.toAddSubgroup` `Ring.toAddCommGroup` `Algebra.toModule` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingSubgroupsBasis.of_comm` `inter` `mul` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `leftMul`
`toSubmodulesBasis` 📖	mathematical	`SubmodulesRingBasis` `Filter.Eventually` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Algebra.toSMul` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`SubmodulesBasis` `Ring.toAddCommGroup` `CommRing.toRing`	—	`inter`

(root)

Definitions

Name	Category	Theorems
`RingSubgroupsBasis` 📖	CompData	3 math math: `SubmodulesRingBasis.toRing_subgroups_basis`, `Valuation.subgroups_basis`, `RingSubgroupsBasis.of_comm`
`SubmodulesBasis` 📖	CompData	2 math math: `RingFilterBasis.submodulesBasisIsBasis`, `SubmodulesRingBasis.toSubmodulesBasis`
`SubmodulesRingBasis` 📖	CompData	1 math math: `Ideal.adic_basis`

---

← Back to Index