Commit 2025-02-02 10:50 8f1b0576

View on Github →

chore: make ‖x‖ₑ.toReal = ‖x‖ simp (#21327) From LeanAPAP

Estimated changes