Commit 2025-01-28 10:27 20c785e9

View on Github →

chore: use ‖x‖ₑ instead of ↑‖x‖₊ (#20806) Rename lemmas from _nnnorm_/_ennnorm_ to _enorm_ where applicable. Rewrite/golf proofs where necessary.

Estimated changes

modified theorem div_le_egauge_ball
modified theorem div_le_egauge_closedBall
modified theorem egauge_le_of_mem_smul
modified theorem egauge_le_of_smul_mem
modified theorem egauge_le_of_smul_mem_of_ne
modified theorem egauge_lt_iff
modified theorem le_egauge_ball_one
modified theorem le_egauge_closedBall_one
modified theorem le_egauge_iff