Is there an ENNReal.natCast_div?

Stream: new members

[Ching-Tsun Chou]

Is there a theorem like:

ENNReal.natCast_sub

but with the subtraction replaced by division and perhaps a side-condition that the divisor must be positive?

[Yaël Dillies]

1 / 2 = 0 in ℕ, so no there isn't. One could state ↑(a / b) = ↑a / ↑b if b ∣ a, but we don't seem to have that either. PR welcome!

[Ching-Tsun Chou]

Good point. I think the a and b in a/b are cast to Real first before the /. So I was looking at the wrong theorems.

[Igor Khavkine]

FYI, here's something like a response to the original request:

import Mathlib.Data.Rat.Init
import Mathlib.Data.ENNReal.Inv

def ENNReal.natCast_div (m n : ℕ) (hn : n ≠ 0) : ↑(NNRat.divNat m n) = (↑m : ENNReal) / ↑n := by
  have recast_rat (nnr : NNRat) : ↑nnr = (↑(↑nnr : NNReal) : ENNReal) := rfl
  have recast_nat (n : Nat) : ↑n = (↑(↑(↑n : NNRat) : NNReal) : ENNReal) := rfl
  repeat rw [recast_nat]
  rw [recast_rat, ← ENNReal.coe_div, ← NNRat.cast_div]
  congr; exact NNRat.cast_divNat _ _
  norm_cast

[Ching-Tsun Chou]

Thanks! In the end I figured out what lemma I actually needed:
#new members > How do I prove this lemma?