Theorem seminormFromBounded_nonzero

Modification history

2026-10-26 16:38

Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean

chore: rename `nonzero` to `ne_zero` in theorem names (#44824) …

Deleted seminormFromBounded_nonzero View on Github →

2024-07-18 08:58

Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean

feat(Analysis.Normed.Ring.SeminormFromBounded): add SeminormFromBounded (#14359) …

Added seminormFromBounded_nonzero View on Github →