Commit 2025-03-25 09:33 b54b0ed6

View on Github →

feat(Valued/NormedValued): add lemma on positivity of the norm (#23277) co-authored with María Inés de Frutos Fernández @mariainesdff

Estimated changes

added theorem Valued.norm_def