Commit 2025-01-07 09:21 1a9143ba

View on Github →

chore(*): replace no_index (ofNat n) with ofNat(n) everywhere (#20521) This PR was made by searching for no_index.*ofNat and replacing all of the relevant occurrences with ofNat(n). This is a rather naïve approach, but at least puts everything back in the same notation for easier applying and reviewing of later fixes.

Estimated changes

modified theorem OfNat.ofNat_ne_one
modified theorem OfNat.ofNat_ne_zero
modified theorem OfNat.one_ne_ofNat
modified theorem OfNat.zero_ne_ofNat
modified theorem Polynomial.ofNat_comp
modified theorem Complex.ofNat_mem_slitPlane
modified theorem Complex.ofNat_arg
modified theorem ENat.map_ofNat
modified theorem ENat.ofNat_ne_top
modified theorem ENat.toNat_ofNat
modified theorem ENat.top_ne_ofNat
modified theorem ENat.top_sub_ofNat
modified theorem NNRat.den_ofNat
modified theorem NNRat.num_ofNat
modified theorem Nat.cast_le_ofNat
modified theorem Nat.cast_lt_ofNat
modified theorem Nat.not_ofNat_le_one
modified theorem Nat.not_ofNat_lt_one
modified theorem Nat.ofNat_le_cast
modified theorem Nat.ofNat_lt_cast
modified theorem Nat.ofNat_nonneg'
modified theorem Nat.one_le_ofNat
modified theorem Nat.one_lt_ofNat
modified theorem PartENat.dom_ofNat
modified theorem PartENat.get_ofNat'
modified theorem PartENat.ofENat_ofNat
modified theorem PartENat.ofNat_lt_top
modified theorem PartENat.ofNat_ne_top
modified theorem NNRat.cast_le_ofNat
modified theorem NNRat.cast_lt_ofNat
modified theorem NNRat.ofNat_le_cast
modified theorem NNRat.ofNat_lt_cast
modified theorem Rat.inv_ofNat_num
modified theorem Rat.sqrt_ofNat
modified theorem Zsqrtd.ofNat_im
modified theorem Zsqrtd.ofNat_re
modified theorem Ordinal.preOmega_ofNat
modified theorem Cardinal.aleph0_add_ofNat
modified theorem Cardinal.aleph0_mul_ofNat
modified theorem Cardinal.ofNat_add_aleph0
modified theorem Cardinal.ofNat_mul_aleph0
modified theorem Cardinal.ord_ofNat