feat(Analysis/SpecialFunctions/Pow): prove (f : α → ℝ) ^ (0 : ℝ) = 1 (#35083)

Prove `pi_rpow_zero (f : α → ℝ) : f ^ (0 : ℝ) = 1`.

Author: vasnesterov

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -121,6 +121,9 @@ theorem rpow_zero (x : ℝ) : x ^ (0 : ℝ) = 1 := by simp [rpow_def]
 
 theorem rpow_zero_pos (x : ℝ) : 0 < x ^ (0 : ℝ) := by simp
 
+@[simp]
+theorem pi_rpow_zero {α : Type*} (f : α → ℝ) : f ^ (0 : ℝ) = 1 := by ext; simp
+
 @[simp]
 theorem zero_rpow {x : ℝ} (h : x ≠ 0) : (0 : ℝ) ^ x = 0 := by simp [rpow_def, *]