Mathlib v3 is deprecated. Go to Mathlib v4

Theorem norm'_eq_zero_iff

Modification history

2021-11-28 07:21
src/analysis/normed_space/hahn_banach.lean
chore(analysis/normed_space/hahn_banach): remove `norm'` (#10527) …
Deleted norm'_eq_zero_iffView on Github →
2021-06-18 18:18
src/analysis/normed_space/hahn_banach.lean
chore(topology/basic): rename compact_Icc to is_compact_Icc (#7979) …
Added norm'_eq_zero_iffView on Github →