Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-24 22:07 f056468f

View on Github →

chore(analysis/normed_space): add 2 @[simp] attrs (#4775) Add @[simp] to norm_pos_iff and norm_le_zero_iff

Estimated changes

modified theorem norm_le_zero_iff
modified theorem norm_pos_iff