Commit 2023-12-04 12:41 070be719

View on Github →

fix: add missing no_index around OfNat.ofNat (#8317)

Estimated changes

modified theorem Int.ceil_add_ofNat
modified theorem Int.ceil_ofNat
modified theorem Int.ceil_sub_ofNat
modified theorem Int.floor_ofNat
modified theorem Int.fract_add_ofNat
modified theorem Int.fract_ofNat
modified theorem Int.fract_ofNat_add
modified theorem Int.fract_sub_ofNat
modified theorem round_ofNat
modified theorem ENat.toENNReal_ofNat
modified theorem Hyperreal.coe_ofNat
modified theorem Cardinal.toNat_ofNat