Theorem Complex.canonicalFactor_apply_self

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.canonicalFactor_apply_selfView on Github →