Commit 2025-01-02 08:45 ac415859

View on Github →

chore: use ofNat() around Real and Complex (#20388) In the places where no_index was not present, this makes these lemmas (or mostly, their reverse) work with simp.

Estimated changes

modified theorem RCLike.conj_ofNat
modified theorem RCLike.nnnorm_ofNat
modified theorem RCLike.norm_ofNat
modified theorem RCLike.ofNat_im
modified theorem RCLike.ofNat_re
modified theorem RCLike.ofReal_ofNat
modified theorem Complex.conj_ofNat
modified theorem Complex.im_ofNat
modified theorem Complex.ofReal_ofNat
modified theorem Complex.re_ofNat
modified theorem ENNReal.coe_ofNat
modified theorem ENNReal.ofNat_lt_top
modified theorem ENNReal.ofNat_ne_top
modified theorem ENNReal.ofReal_ofNat
modified theorem ENNReal.toReal_ofNat
modified theorem ENat.toENNReal_ofNat
modified theorem Irrational.ne_ofNat
modified theorem not_irrational_ofNat