Theorem Complex.analyticOnNhd_canonicalFactor

Modification history

2026-03-18 18:34
Mathlib/Analysis/Complex/CanonicalDecomposition.lean
feat: introduce canonical factors, a.k.a. "Blaschke factors", as used in complex analysis (#36264) …
Added Complex.analyticOnNhd_canonicalFactorView on Github →