Theorem Int.norm_coe_units

Modification history

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