Commit 2023-04-04 12:40 52e74692

View on Github →

feat: port Topology.UniformSpace.Matrix (#3262)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Matrix.lean

added theorem Matrix.uniformContinuous

added theorem Matrix.uniformity