TODO: rename `pseudometric` #1990

Open

Labels

renaming/refactoring 🔧

Milestone

opened

analysis/theories/topology_theory/pseudometric_structure.v

Line 77 in 723425a

#[short(type="pseudoMetricType")]

but how? @CohenCyril @mkerjean

Metadata

Assignees

No one assigned

Labels

renaming/refactoring 🔧

Type

No type

Fields

No fields configured for issues without a type.

Projects

No projects

Milestone

1.18.0

Relationships

None yet

Development

No branches or pull requests