Theorem TietzeExtension.of_tvs

Modification history

2024-02-15 16:15
Mathlib/Analysis/Complex/Tietze.lean
feat: add a `TietzeExtension` class (#9788) …
Added TietzeExtension.of_tvsView on Github →