Def DilationEquiv.refl

Modification history

2023-08-10 19:52

Mathlib/Topology/MetricSpace/DilationEquiv.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified DilationEquiv.refl View on Github →

2023-07-24 10:30

Mathlib/Topology/MetricSpace/DilationEquiv.lean

feat: define `DilationEquiv` (#5755)

Added DilationEquiv.refl View on Github →