Commit 2023-05-18 08:06 17e26bfc

View on Github →

feat: port Analysis.Complex.OperatorNorm (#4065)

Estimated changes

added theorem Complex.conjCle_nnorm
added theorem Complex.conjCle_norm
added theorem Complex.det_conjLie
added theorem Complex.imClm_nnnorm
added theorem Complex.imClm_norm
added theorem Complex.ofRealClm_norm
added theorem Complex.reClm_nnnorm
added theorem Complex.reClm_norm