Theorem Circle.nnnorm_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.nnnorm_coeView on Github →