Theorem Metric.instTietzeExtensionBall

Modification history

2024-03-28 10:26
Mathlib/Analysis/Complex/Tietze.lean
chore: Rename `IsROrC` to `RCLike` (#10819) …
Modified Metric.instTietzeExtensionBallView on Github →
2024-02-15 16:15
Mathlib/Analysis/Complex/Tietze.lean
feat: add a `TietzeExtension` class (#9788) …
Added Metric.instTietzeExtensionBallView on Github →