Basic

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

Statistics

Metric	Count
Definitions NonarchimedeanAddGroup, NonarchimedeanGroup, NonarchimedeanRing	3
Theorems instNonarchimedeanAddGroup, is_nonarchimedean, nonarchimedean_of_emb, prod_self_subset, prod_subset, toIsTopologicalAddGroup, instNonarchimedeanGroup, is_nonarchimedean, nonarchimedean_of_emb, prod_self_subset, prod_subset, toIsTopologicalGroup, instProd, is_nonarchimedean, left_mul_subset, mul_subset, toIsTopologicalRing, to_nonarchimedeanAddGroup	18
Total	21

NonarchimedeanAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_nonarchimedean 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Set.instHasSubset SetLike.coe OpenAddSubgroup OpenAddSubgroup.instSetLike	—	—
nonarchimedean_of_emb 📖	mathematical	Topology.IsOpenEmbedding DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike	NonarchimedeanAddGroup	—	Continuous.tendsto Topology.IsOpenEmbedding.continuous AddMonoidHom.map_zero is_nonarchimedean Topology.IsOpenEmbedding.isOpenMap OpenAddSubgroup.isOpen Set.image_subset_iff
prod_self_subset 📖	mathematical	Set Filter Filter.instMembership nhds instTopologicalSpaceProd Prod.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Set.instHasSubset SProd.sprod Set.instSProd SetLike.coe OpenAddSubgroup OpenAddSubgroup.instSetLike	—	prod_subset Set.Subset.trans Set.prod_mono Set.inter_subset_left Set.inter_subset_right
prod_subset 📖	mathematical	Set Filter Filter.instMembership nhds instTopologicalSpaceProd Prod.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Set.instHasSubset SProd.sprod Set.instSProd SetLike.coe OpenAddSubgroup OpenAddSubgroup.instSetLike	—	Filter.mem_prod_iff nhds_prod_eq is_nonarchimedean
toIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup	—	—

NonarchimedeanAddGroup.Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonarchimedeanAddGroup 📖	mathematical	—	NonarchimedeanAddGroup Prod.instAddGroup instTopologicalSpaceProd	—	Prod.instIsTopologicalAddGroup NonarchimedeanAddGroup.toIsTopologicalAddGroup NonarchimedeanAddGroup.prod_subset

NonarchimedeanGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_nonarchimedean 📖	mathematical	Set Filter Filter.instMembership nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Set.instHasSubset SetLike.coe OpenSubgroup OpenSubgroup.instSetLike	—	—
nonarchimedean_of_emb 📖	mathematical	Topology.IsOpenEmbedding DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	NonarchimedeanGroup	—	Continuous.tendsto Topology.IsOpenEmbedding.continuous MonoidHom.map_one is_nonarchimedean Topology.IsOpenEmbedding.isOpenMap OpenSubgroup.isOpen Set.image_subset_iff
prod_self_subset 📖	mathematical	Set Filter Filter.instMembership nhds instTopologicalSpaceProd Prod.instOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Set.instHasSubset SProd.sprod Set.instSProd SetLike.coe OpenSubgroup OpenSubgroup.instSetLike	—	prod_subset Set.Subset.trans Set.prod_mono
prod_subset 📖	mathematical	Set Filter Filter.instMembership nhds instTopologicalSpaceProd Prod.instOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Set.instHasSubset SProd.sprod Set.instSProd SetLike.coe OpenSubgroup OpenSubgroup.instSetLike	—	Filter.mem_prod_iff nhds_prod_eq is_nonarchimedean
toIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup	—	—

NonarchimedeanGroup.Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonarchimedeanGroup 📖	mathematical	—	NonarchimedeanGroup Prod.instGroup instTopologicalSpaceProd	—	Prod.instIsTopologicalGroup NonarchimedeanGroup.toIsTopologicalGroup NonarchimedeanGroup.prod_subset

NonarchimedeanRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instProd 📖	mathematical	—	NonarchimedeanRing Prod.instRing instTopologicalSpaceProd	—	instIsTopologicalRingProd toIsTopologicalRing NonarchimedeanAddGroup.is_nonarchimedean NonarchimedeanAddGroup.Prod.instNonarchimedeanAddGroup to_nonarchimedeanAddGroup
is_nonarchimedean 📖	mathematical	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set.instHasSubset SetLike.coe OpenAddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne OpenAddSubgroup.instSetLike	—	—
left_mul_subset 📖	mathematical	—	Set Set.instHasSubset Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SetLike.coe OpenAddSubgroup AddGroupWithOne.toAddGroup OpenAddSubgroup.instSetLike	—	continuous_mul_left IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring toIsTopologicalRing Set.image_preimage_subset
mul_subset 📖	mathematical	—	Set Set.instHasSubset Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SetLike.coe OpenAddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne OpenAddSubgroup.instSetLike	—	NonarchimedeanAddGroup.prod_self_subset to_nonarchimedeanAddGroup IsOpen.mem_nhds IsOpen.preimage continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring toIsTopologicalRing OpenAddSubgroup.isOpen MulZeroClass.mul_zero AddSubgroup.zero_mem Set.mk_mem_prod SetLike.mem_coe
toIsTopologicalRing 📖	mathematical	—	IsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
to_nonarchimedeanAddGroup 📖	mathematical	—	NonarchimedeanAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring toIsTopologicalRing IsTopologicalRing.toContinuousNeg is_nonarchimedean

(root)

Definitions

Name	Category	Theorems
NonarchimedeanAddGroup 📖	CompData	6 math math: NonarchimedeanRing.to_nonarchimedeanAddGroup, IsUltrametricDist.nonarchimedeanAddGroup, instNonarchimedeanAddGroupCompletion, SubmodulesBasis.nonarchimedean, NonarchimedeanAddGroup.nonarchimedean_of_emb, NonarchimedeanAddGroup.Prod.instNonarchimedeanAddGroup
NonarchimedeanGroup 📖	CompData	3 math math: NonarchimedeanGroup.Prod.instNonarchimedeanGroup, NonarchimedeanGroup.nonarchimedean_of_emb, IsUltrametricDist.nonarchimedeanGroup
NonarchimedeanRing 📖	CompData	5 math math: Ideal.nonarchimedean, NonarchimedeanRing.instProd, instNonarchimedeanRingCompletion, WithIdeal.instNonarchimedeanRing, RingSubgroupsBasis.nonarchimedean

---

← Back to Index