Mathlib Changelog
v4
Changelog
About
Github
Def
Dilation.ratioHom
Modification history
2023-07-21 14:16
Mathlib/Topology/MetricSpace/Dilation.lean
refactor: add notation for `Dilation _ _`, extend API (#5753) …
Added
Dilation.ratioHom
View on Github →