mathlib
f056468f - chore(analysis/normed_space): add 2 `@[simp]` attrs (#4775)

Commit

5 years ago

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

References

Author

urkud

Parents