Commit 2024-08-29 12:34 3eea6357

View on Github →

feat(RCLike): nnnorm lemmas (#16144) From LeanAPAP

Estimated changes

deleted theorem Complex.nnnorm_int
added theorem Complex.nnnorm_intCast
deleted theorem Complex.nnnorm_nat
added theorem Complex.nnnorm_natCast
added theorem Complex.nnnorm_ofNat
added theorem Complex.nnnorm_ratCast
modified theorem Complex.nnnorm_real
deleted theorem Complex.norm_int
added theorem Complex.norm_intCast
deleted theorem Complex.norm_nat
added theorem Complex.norm_natCast
added theorem Complex.norm_nnratCast
added theorem Complex.norm_ofNat
deleted theorem Complex.norm_rat
added theorem Complex.norm_ratCast
modified theorem Complex.norm_real
modified theorem Real.nnnorm_natCast
added theorem Real.nnnorm_nnratCast
added theorem Real.nnnorm_ofNat
modified theorem Real.nnnorm_two
modified theorem Real.norm_natCast
added theorem Real.norm_nnratCast
added theorem Real.norm_ofNat
modified theorem Real.norm_two
added theorem RCLike.nnnorm_conj
added theorem RCLike.nnnorm_natCast
added theorem RCLike.nnnorm_nnqsmul
added theorem RCLike.nnnorm_nsmul
added theorem RCLike.nnnorm_ofNat
added theorem RCLike.nnnorm_two
modified theorem RCLike.norm_conj
added theorem RCLike.norm_nnqsmul
added theorem RCLike.norm_nnratCast
modified theorem RCLike.norm_two