Theorem nontrivialTopology_iff_exists_norm_ne_zero'

Modification history

2026-01-28 19:17
Mathlib/Analysis/Normed/Group/Basic.lean
feat: add a typeclass for the indiscrete topology (#29120) …
Added nontrivialTopology_iff_exists_norm_ne_zero'View on Github →