Documentation Verification Report

FilterBasis

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

Statistics

Metric	Count
Definitions `AddGroupFilterBasis`, `N`, `instInhabited`, `instMembershipSet`, `toFilterBasis`, `topology`, `FilterBasis`, `GroupFilterBasis`, `N`, `instInhabited`, `instMembershipSet`, `toFilterBasis`, `topology`, `ModuleFilterBasis`, `hasMem`, `instInhabitedOfDiscreteTopology`, `ofBases`, `toAddGroupFilterBasis`, `topology`, `topology'`, `RingFilterBasis`, `instMembershipSet`, `toAddGroupFilterBasis`, `topology`, `addGroupFilterBasisOfComm`, `groupFilterBasisOfComm`	26
Theorems `N_zero`, `add`, `add'`, `conj`, `conj'`, `hasBasis`, `isTopologicalAddGroup`, `mem_nhds_zero`, `neg`, `neg'`, `nhds_eq`, `nhds_hasBasis`, `nhds_zero_eq`, `nhds_zero_hasBasis`, `subset_add_self`, `t2Space_iff`, `t2Space_iff_sInter_subset`, `zero`, `zero'`, `of_basis_zero`, `N_one`, `conj`, `conj'`, `hasBasis`, `inv`, `inv'`, `isTopologicalGroup`, `mem_nhds_one`, `mul`, `mul'`, `nhds_eq`, `nhds_hasBasis`, `nhds_one_eq`, `nhds_one_hasBasis`, `one`, `one'`, `subset_mul_self`, `t2Space_iff`, `t2Space_iff_sInter_subset`, `continuousSMul`, `smul`, `smul'`, `smul_left`, `smul_left'`, `smul_right`, `smul_right'`, `isTopologicalRing`, `mul`, `mul'`, `mul_left`, `mul_left'`, `mul_right`, `mul_right'`	53
Total	79

AddGroupFilterBasis

Definitions

Name	Category	Theorems
`N` 📖	CompOp	3 math math: `nhds_eq`, `N_zero`, `hasBasis`
`instInhabited` 📖	CompOp	—
`instMembershipSet` 📖	CompOp	5 math math: `nhds_hasBasis`, `RingSubgroupsBasis.mem_addGroupFilterBasis`, `hasBasis`, `nhds_zero_hasBasis`, `RingSubgroupsBasis.mem_addGroupFilterBasis_iff`
`toFilterBasis` 📖	CompOp	9 math math: `t2Space_iff`, `IdealFilter.ringFilterBasis_sets`, `SeminormFamily.filter_eq_iInf`, `N_zero`, `nhds_zero_eq`, `SeminormFamily.basisSets_smul`, `t2Space_iff_sInter_subset`, `IdealFilter.isUniform_iff_exists_ringFilterBasis`, `SeminormFamily.basisSets_smul_left`
`topology` 📖	CompOp	6 math math: `nhds_hasBasis`, `isTopologicalAddGroup`, `nhds_eq`, `nhds_zero_eq`, `nhds_zero_hasBasis`, `mem_nhds_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`N_zero` 📖	mathematical	—	`N` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `FilterBasis.filter` `toFilterBasis`	—	`zero_add` `Filter.map_id'`
`add` 📖	mathematical	`Set` `AddGroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add'`
`add'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`Set.instHasSubset` `Set.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`conj` 📖	mathematical	`Set` `AddGroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`conj'`
`conj'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`Set.instHasSubset` `Set.preimage` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`hasBasis` 📖	mathematical	—	`Filter.HasBasis` `Set` `N` `AddGroupFilterBasis` `instMembershipSet` `Set.image` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Filter.HasBasis.map` `FilterBasis.hasBasis`
`isTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `topology`	—	`nhds_zero_hasBasis` `Filter.HasBasis.prod` `IsTopologicalAddGroup.of_nhds_zero` `Filter.HasBasis.tendsto_iff` `add` `Set.add_mem_add` `Set.mem_prod` `neg` `nhds_eq` `nhds_zero_eq` `conj`
`mem_nhds_zero` 📖	mathematical	`Set` `AddGroupFilterBasis` `instMembershipSet`	`Filter` `Filter.instMembership` `nhds` `topology` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Filter.HasBasis.mem_iff` `nhds_zero_hasBasis` `Eq.subset` `Set.instReflSubset`
`neg` 📖	mathematical	`Set` `AddGroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.preimage` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg'`
`neg'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`Set.instHasSubset` `Set.preimage` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`nhds_eq` 📖	mathematical	—	`nhds` `topology` `N`	—	`TopologicalSpace.nhds_mkOfNhds_of_hasBasis` `Filter.HasBasis.map` `FilterBasis.hasBasis` `zero` `add_zero` `add` `Filter.mp_mem` `Filter.image_mem_map` `FilterBasis.mem_filter_of_mem` `Filter.univ_mem'` `Filter.vadd_set_mem_vadd_filter` `vadd_vadd` `Set.vadd_set_mono` `Set.vadd_set_subset_vadd`
`nhds_hasBasis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `topology` `AddGroupFilterBasis` `instMembershipSet` `Set.image` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`nhds_eq` `hasBasis`
`nhds_zero_eq` 📖	mathematical	—	`nhds` `topology` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `FilterBasis.filter` `toFilterBasis`	—	`nhds_eq` `zero_add` `Filter.map_id`
`nhds_zero_hasBasis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `topology` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupFilterBasis` `instMembershipSet`	—	`nhds_zero_eq` `FilterBasis.hasBasis`
`subset_add_self` 📖	mathematical	`Set` `AddGroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`zero` `zero_add`
`t2Space_iff` 📖	mathematical	`topology`	`T2Space` `Set.sInter` `FilterBasis.sets` `toFilterBasis` `Set` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`isTopologicalAddGroup` `IsTopologicalAddGroup.t2Space_iff_zero_closed` `closure_eq_iff_isClosed` `R0Space.closure_singleton` `instR0Space` `instR1Space` `IsTopologicalAddGroup.regularSpace` `nhds_zero_eq` `FilterBasis.ker_filter`
`t2Space_iff_sInter_subset` 📖	mathematical	`topology`	`T2Space` `Set` `Set.instHasSubset` `Set.sInter` `FilterBasis.sets` `toFilterBasis` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`t2Space_iff` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `Set.subset_sInter_iff` `FilterBasis.mem_sets` `Set.singleton_subset_iff` `zero`
`zero` 📖	mathematical	`Set` `AddGroupFilterBasis` `instMembershipSet`	`Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`zero'`
`zero'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

ContinuousSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_basis_zero` 📖	mathematical	`Filter.HasBasis` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Filter` `Filter.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Set.instHasSubset` `Set.smul` `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` `Set.MapsTo` `Filter.Eventually` `Set.instMembership`	`ContinuousSMul`	—	`of_nhds_zero` `Filter.HasBasis.tendsto_right_iff` `Filter.mem_of_superset` `Filter.prod_mem_prod` `Filter.HasBasis.mem_of_mem` `Set.smul_mem_smul`

GroupFilterBasis

Definitions

Name	Category	Theorems
`N` 📖	CompOp	3 math math: `hasBasis`, `N_one`, `nhds_eq`
`instInhabited` 📖	CompOp	—
`instMembershipSet` 📖	CompOp	3 math math: `nhds_hasBasis`, `hasBasis`, `nhds_one_hasBasis`
`toFilterBasis` 📖	CompOp	4 math math: `nhds_one_eq`, `t2Space_iff_sInter_subset`, `N_one`, `t2Space_iff`
`topology` 📖	CompOp	6 math math: `nhds_hasBasis`, `nhds_one_eq`, `mem_nhds_one`, `isTopologicalGroup`, `nhds_one_hasBasis`, `nhds_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`N_one` 📖	mathematical	—	`N` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `FilterBasis.filter` `toFilterBasis`	—	`one_mul` `Filter.map_id'`
`conj` 📖	mathematical	`Set` `GroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`conj'`
`conj'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`Set.instHasSubset` `Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`hasBasis` 📖	mathematical	—	`Filter.HasBasis` `Set` `N` `GroupFilterBasis` `instMembershipSet` `Set.image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Filter.HasBasis.map` `FilterBasis.hasBasis`
`inv` 📖	mathematical	`Set` `GroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.preimage` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv'`
`inv'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`Set.instHasSubset` `Set.preimage` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`isTopologicalGroup` 📖	mathematical	—	`IsTopologicalGroup` `topology`	—	`nhds_one_hasBasis` `Filter.HasBasis.prod` `IsTopologicalGroup.of_nhds_one` `Filter.HasBasis.tendsto_iff` `mul` `Set.mul_mem_mul` `inv` `nhds_eq` `nhds_one_eq` `conj`
`mem_nhds_one` 📖	mathematical	`Set` `GroupFilterBasis` `instMembershipSet`	`Filter` `Filter.instMembership` `nhds` `topology` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Filter.HasBasis.mem_iff` `nhds_one_hasBasis` `Eq.subset` `Set.instReflSubset`
`mul` 📖	mathematical	`Set` `GroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul'`
`mul'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`nhds_eq` 📖	mathematical	—	`nhds` `topology` `N`	—	`TopologicalSpace.nhds_mkOfNhds_of_hasBasis` `Filter.HasBasis.map` `FilterBasis.hasBasis` `one` `mul_one` `mul` `Filter.mp_mem` `Filter.image_mem_map` `FilterBasis.mem_filter_of_mem` `Filter.univ_mem'` `Filter.smul_set_mem_smul_filter` `smul_smul` `Set.smul_set_mono` `Set.smul_set_subset_smul`
`nhds_hasBasis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `topology` `GroupFilterBasis` `instMembershipSet` `Set.image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`nhds_eq` `hasBasis`
`nhds_one_eq` 📖	mathematical	—	`nhds` `topology` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `FilterBasis.filter` `toFilterBasis`	—	`nhds_eq` `one_mul` `Filter.map_id`
`nhds_one_hasBasis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `topology` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `GroupFilterBasis` `instMembershipSet`	—	`nhds_one_eq` `FilterBasis.hasBasis`
`one` 📖	mathematical	`Set` `GroupFilterBasis` `instMembershipSet`	`Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`one'`
`one'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `toFilterBasis`	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`subset_mul_self` 📖	mathematical	`Set` `GroupFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`one` `one_mul`
`t2Space_iff` 📖	mathematical	`topology`	`T2Space` `Set.sInter` `FilterBasis.sets` `toFilterBasis` `Set` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`isTopologicalGroup` `IsTopologicalGroup.t2Space_iff_one_closed` `closure_eq_iff_isClosed` `R0Space.closure_singleton` `instR0Space` `instR1Space` `IsTopologicalGroup.regularSpace` `nhds_one_eq` `FilterBasis.ker_filter`
`t2Space_iff_sInter_subset` 📖	mathematical	`topology`	`T2Space` `Set` `Set.instHasSubset` `Set.sInter` `FilterBasis.sets` `toFilterBasis` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`t2Space_iff` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `one`

ModuleFilterBasis

Definitions

Name	Category	Theorems
`instInhabitedOfDiscreteTopology` 📖	CompOp	—
`ofBases` 📖	CompOp	—
`toAddGroupFilterBasis` 📖	CompOp	1 math math: `SeminormFamily.filter_eq_iInf`
`topology` 📖	CompOp	3 math math: `WithSeminorms.withSeminorms_eq`, `WithSeminorms.topology_eq_withSeminorms`, `continuousSMul`
`topology'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `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` `topology`	—	`AddGroupFilterBasis.isTopologicalAddGroup` `ContinuousSMul.of_basis_zero` `AddGroupFilterBasis.nhds_zero_hasBasis` `smul` `smul_left` `smul_right`
`smul` 📖	mathematical	`Set` `ModuleFilterBasis` `GroupFilterBasis.hasMem`	`Filter` `Filter.instMembership` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Set.instHasSubset` `Set.smul` `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`	—	`smul'`
`smul'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `AddGroupFilterBasis.toFilterBasis` `AddCommGroup.toAddGroup` `toAddGroupFilterBasis`	`Filter` `Filter.instMembership` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Set.instHasSubset` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	—
`smul_left` 📖	mathematical	`Set` `ModuleFilterBasis` `GroupFilterBasis.hasMem`	`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`	—	`smul_left'`
`smul_left'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `AddGroupFilterBasis.toFilterBasis` `AddCommGroup.toAddGroup` `toAddGroupFilterBasis`	`Set.instHasSubset` `Set.preimage` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	—
`smul_right` 📖	mathematical	`Set` `ModuleFilterBasis` `GroupFilterBasis.hasMem`	`Filter.Eventually` `Set.instMembership` `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` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smul_right'`
`smul_right'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `AddGroupFilterBasis.toFilterBasis` `AddCommGroup.toAddGroup` `toAddGroupFilterBasis`	`Filter.Eventually` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—

ModuleFilterBasis.GroupFilterBasis

Definitions

Name	Category	Theorems
`hasMem` 📖	CompOp	—

RingFilterBasis

Definitions

Name	Category	Theorems
`instMembershipSet` 📖	CompOp	1 math math: `SubmodulesBasis.smul`
`toAddGroupFilterBasis` 📖	CompOp	5 math math: `IdealFilter.ringFilterBasis_sets`, `Valued.toUniformSpace_eq`, `RingSubgroupsBasis.mem_addGroupFilterBasis`, `RingSubgroupsBasis.mem_addGroupFilterBasis_iff`, `IdealFilter.isUniform_iff_exists_ringFilterBasis`
`topology` 📖	CompOp	2 math math: `isTopologicalRing`, `submodulesBasisIsBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `topology` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`AddGroupFilterBasis.nhds_zero_hasBasis` `Filter.HasBasis.prod` `IsTopologicalRing.of_addGroup_of_nhds_zero` `AddGroupFilterBasis.isTopologicalAddGroup` `Filter.HasBasis.tendsto_iff` `mul` `Set.mul_mem_mul` `mul_left` `mul_right`
`mul` 📖	mathematical	`Set` `RingFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`mul'`
`mul'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `AddGroupFilterBasis.toFilterBasis` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toAddGroupFilterBasis`	`Set.instHasSubset` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`mul_left` 📖	mathematical	`Set` `RingFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`mul_left'`
`mul_left'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `AddGroupFilterBasis.toFilterBasis` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toAddGroupFilterBasis`	`Set.instHasSubset` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`mul_right` 📖	mathematical	`Set` `RingFilterBasis` `instMembershipSet`	`Set.instHasSubset` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`mul_right'`
`mul_right'` 📖	mathematical	`Set` `Set.instMembership` `FilterBasis.sets` `AddGroupFilterBasis.toFilterBasis` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toAddGroupFilterBasis`	`Set.instHasSubset` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—

(root)

Definitions

Name	Category	Theorems
`AddGroupFilterBasis` 📖	CompData	5 math math: `AddGroupFilterBasis.nhds_hasBasis`, `RingSubgroupsBasis.mem_addGroupFilterBasis`, `AddGroupFilterBasis.hasBasis`, `AddGroupFilterBasis.nhds_zero_hasBasis`, `RingSubgroupsBasis.mem_addGroupFilterBasis_iff`
`FilterBasis` 📖	CompData	6 math math: `FilterBasis.hasBasis`, `Filter.IsBasis.mem_filterBasis_iff`, `FilterBasis.mem_filter_iff`, `mem_galBasis_iff`, `UniformOnFun.isBasis_gen`, `FilterBasis.mem_sets`
`GroupFilterBasis` 📖	CompData	3 math math: `GroupFilterBasis.nhds_hasBasis`, `GroupFilterBasis.hasBasis`, `GroupFilterBasis.nhds_one_hasBasis`
`ModuleFilterBasis` 📖	CompData	—
`RingFilterBasis` 📖	CompData	1 math math: `RingFilterBasis.SubmodulesBasis.smul`
`addGroupFilterBasisOfComm` 📖	CompOp	—
`groupFilterBasisOfComm` 📖	CompOp	—

---

← Back to Index