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', addConj, 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	8 math math: nhds_hasBasis, addConj, neg, RingSubgroupsBasis.mem_addGroupFilterBasis, hasBasis, nhds_zero_hasBasis, RingSubgroupsBasis.mem_addGroupFilterBasis_iff, add
toFilterBasis 📖	CompOp	17 math math: t2Space_iff, IdealFilter.ringFilterBasis_sets, SeminormFamily.filter_eq_iInf, neg', add', conj', ModuleFilterBasis.smul_left', N_zero, RingFilterBasis.mul_left', RingFilterBasis.mul', nhds_zero_eq, SeminormFamily.basisSets_smul, ModuleFilterBasis.smul', RingFilterBasis.mul_right', 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 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 Set.instMembership FilterBasis.sets toFilterBasis Set.instHasSubset Set.add AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
addConj 📖	mathematical	Set AddGroupFilterBasis instMembershipSet	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 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 addConj
mem_nhds_zero 📖	mathematical	Set AddGroupFilterBasis instMembershipSet	Set 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 AddGroupFilterBasis instMembershipSet Set.instHasSubset Set.preimage NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg'
neg' 📖	mathematical	Set Set.instMembership FilterBasis.sets toFilterBasis	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 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 Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zero'
zero' 📖	mathematical	Set Set.instMembership FilterBasis.sets toFilterBasis	Set Set.instMembership 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 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	—	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	6 math math: conj, nhds_hasBasis, mul, hasBasis, nhds_one_hasBasis, inv
toFilterBasis 📖	CompOp	7 math math: nhds_one_eq, t2Space_iff_sInter_subset, conj', mul', N_one, inv', 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 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 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 GroupFilterBasis instMembershipSet Set.instHasSubset Set.preimage InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv'
inv' 📖	mathematical	Set Set.instMembership FilterBasis.sets toFilterBasis	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	Set 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 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 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 Set.instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one'
one' 📖	mathematical	Set Set.instMembership FilterBasis.sets toFilterBasis	Set Set.instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
subset_mul_self 📖	mathematical	Set GroupFilterBasis instMembershipSet	Set 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	3 math math: SeminormFamily.filter_eq_iInf, smul_left', smul'
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	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ModuleFilterBasis GroupFilterBasis.hasMem 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	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.instMembership FilterBasis.sets AddGroupFilterBasis.toFilterBasis AddCommGroup.toAddGroup toAddGroupFilterBasis 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 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 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 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 Set 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	—	—

ModuleFilterBasis.GroupFilterBasis

Definitions

Name	Category	Theorems
hasMem 📖	CompOp	2 math math: ModuleFilterBasis.smul_left, ModuleFilterBasis.smul

RingFilterBasis

Definitions

Name	Category	Theorems
instMembershipSet 📖	CompOp	4 math math: mul_left, mul_right, mul, SubmodulesBasis.smul
toAddGroupFilterBasis 📖	CompOp	9 math math: IdealFilter.ringFilterBasis_sets, Valued.toUniformSpace_eq, mul_left', mul', RingSubgroupsBasis.mem_addGroupFilterBasis, mul_right', Valuation.toUniformSpace_eq, 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 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 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 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 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 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 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	8 math math: AddGroupFilterBasis.nhds_hasBasis, AddGroupFilterBasis.addConj, AddGroupFilterBasis.neg, RingSubgroupsBasis.mem_addGroupFilterBasis, AddGroupFilterBasis.hasBasis, AddGroupFilterBasis.nhds_zero_hasBasis, RingSubgroupsBasis.mem_addGroupFilterBasis_iff, AddGroupFilterBasis.add
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	6 math math: GroupFilterBasis.conj, GroupFilterBasis.nhds_hasBasis, GroupFilterBasis.mul, GroupFilterBasis.hasBasis, GroupFilterBasis.nhds_one_hasBasis, GroupFilterBasis.inv
ModuleFilterBasis 📖	CompData	2 math math: ModuleFilterBasis.smul_left, ModuleFilterBasis.smul
RingFilterBasis 📖	CompData	5 math math: RingFilterBasis.mul_left, RingFilterBasis.mul_right, RingFilterBasis.mul, IdealFilter.isUniform_iff_exists_ringFilterBasis, RingFilterBasis.SubmodulesBasis.smul
addGroupFilterBasisOfComm 📖	CompOp	—
groupFilterBasisOfComm 📖	CompOp	—

---

← Back to Index