Theorem Real.rpow_ne_zero

Modification history

2025-05-13 15:48
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
chore: remove some `simp` attributes on lemmas that `simp [*]` can prove (#24851)
Modified Real.rpow_ne_zeroView on Github →
2024-05-06 07:35
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat(Analysis/SpecialFunctions/Pow/Real): rpow_ne_zero (#12428)
Added Real.rpow_ne_zeroView on Github →