Commit 2024-09-02 14:00 171d7e04

View on Github →

feat: ‖I‖₊ = 1 (#16407) From LeanAPAP

Estimated changes

added theorem Complex.nnnorm_I