Real.rpow_ne_one formerly in this file follows from mathlib's Real.rpow_right_inj (a ^ b = a ^ 0 = 1 ↔ b = 0 for 0 < a, a ≠ 1).