`BookProof.SymmetryEntropy.negMulLog_eq_zero_iff` {x : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) : Real.negMulLog x = 0 ↔ x = 0 ∨ x = 1

Initializing...

`BookProof.SymmetryEntropy.negMulLog_eq_zero_iff` {x : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) : Real.negMulLog x = 0 ↔ x = 0 ∨ x = 1 · Prove2Me