Theorem Prod.nnnorm_mk'

Modification history

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