Commit 2024-11-28 04:54 73295cb7

View on Github →

feat(Normed/Group): add norm_abs_zsmul and norm_neg_one_pow_zsmul (#19541)

Estimated changes

modified theorem coe_nnnorm'
modified theorem nnnorm_one'
added theorem nnnorm_pow_natAbs
added theorem nnnorm_units_zsmul
added theorem nnnorm_zpow_abs
added theorem nnnorm_zpow_isUnit
added theorem norm_pow_natAbs
added theorem norm_units_zsmul
added theorem norm_zpow_abs
added theorem norm_zpow_isUnit