Theorem Int.nnnorm_coe_units

Modification history

2023-03-13 15:40
Mathlib/Analysis/NormedSpace/Int.lean
feat: port Analysis.NormedSpace.Int (#2848)
Added Int.nnnorm_coe_unitsView on Github →