Theorem Valued.norm_pos_iff_valuation_pos

Modification history

2026-03-06 17:55
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore(Topology/Algebra/Valued/NormedValued): replace Valued.norm by Valuation.norm (#36284) …
Deleted Valued.norm_pos_iff_valuation_posView on Github →
2025-03-25 09:33
Mathlib/Topology/Algebra/Valued/NormedValued.lean
feat(Valued/NormedValued): add lemma on positivity of the norm (#23277) …
Added Valued.norm_pos_iff_valuation_posView on Github →