Commit 2023-03-13 15:40 da6451b0

View on Github →

feat: port Analysis.NormedSpace.Int (#2848)

Estimated changes

added theorem Int.nnnorm_coe_nat
added theorem Int.nnnorm_coe_units
added theorem Int.norm_coe_units