Commit 2023-04-18 11:12 bff27912

View on Github →

feat: port Topology.Algebra.Valuation (#3499)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Valuation.lean

added theorem Valuation.subgroups_basis

added theorem Valued.cauchy_iff

added theorem Valued.hasBasis_nhds_zero

added theorem Valued.hasBasis_uniformity

added theorem Valued.loc_const

added theorem Valued.mem_nhds

added theorem Valued.mem_nhds_zero

added def Valued.mk'

added theorem Valued.toUniformSpace_eq