Theorem Prod.norm_mk

Modification history

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