Skip to content

feat(Padics): add an instance IsValuativeTopology ℚ_[p] - #42998

Open
WenrongZou wants to merge 2 commits into
leanprover-community:masterfrom
WenrongZou:ValuativeRel_Qp
Open

feat(Padics): add an instance IsValuativeTopology ℚ_[p]#42998
WenrongZou wants to merge 2 commits into
leanprover-community:masterfrom
WenrongZou:ValuativeRel_Qp

Commits

Commits on Aug 21, 2026