Commit 2026-08-23 08:18 8d56a84a

View on Github →

chore(Analysis/Complex/Circle): nnnorm and enorm lemmas for circle (#43053)

Estimated changes

added theorem Circle.enorm_coe
added theorem Circle.nnnorm_coe
modified theorem Circle.norm_coe