Theorem Prod.nnnorm_def'

Modification history

2025-01-06 22:50
Mathlib/Analysis/Normed/Group/Constructions.lean
feat: add @[simp] lemma Prod.norm_mk (#20411)
Added Prod.nnnorm_def'View on Github →