Algebraic identities for negMulLog

Mathlib's Analysis.SpecialFunctions.Log.NegMulLog has the product identity Real.negMulLog_mul but neither its inverse nor quotient companions (cf. Real.log_inv/Real.log_div beside Real.log_mul). This file completes the family; the division identity is the pointwise step of the entropy chain rule. [UPSTREAM] candidate for that file.

theorem Real.negMulLog_inv (y : ℝ) : y⁻¹.negMulLog = y⁻¹ * log y

theorem Real.negMulLog_div (x : ℝ) {y : ℝ} (hy : y ≠ 0) : y * (x / y).negMulLog = x.negMulLog + x * log y