Commit 2024-02-25 19:55 da1fa193

View on Github →

chore: add instance from Nat.AtLeastTwo n to NeZero n (#10964) This PR cleans up some lemmas where we're taking named instance parameters [h : Nat.AtLeastTwo n] and manually proving inequalities like 0 < n from h by adding an instance of NeZero n from Nat.AtLeastTwo n as well as a couple of other helper lemmas. This removes Nat.AtLeastTwo.ne_zero, as NeZero.ne_zero replaces it.

Estimated changes

modified theorem OfNat.ofNat_ne_one
modified theorem OfNat.ofNat_ne_zero
modified theorem Complex.ofNat_mem_slitPlane
modified theorem Complex.cpow_ofNat_inv_pow
modified theorem Complex.pow_cpow_ofNat_inv
modified theorem ENNReal.ofNat_le_ofReal
modified theorem ENNReal.ofReal_eq_ofNat
modified theorem ENNReal.ofReal_lt_ofNat
modified theorem Nat.AtLeastTwo.ne_one
deleted theorem Nat.AtLeastTwo.ne_zero
added theorem Nat.AtLeastTwo.one_lt
modified theorem Real.ofNat_le_toNNReal
modified theorem Real.toNNReal_eq_ofNat
modified theorem Real.toNNReal_lt_ofNat