Theorem Circle.enorm_coe

Modification history

2026-08-23 08:18
Mathlib/Analysis/Complex/Circle.lean
chore(Analysis/Complex/Circle): nnnorm and enorm lemmas for circle (#43053)
Added Circle.enorm_coeView on Github →