Theorem RCLike.re_ofReal_pow

Modification history

2025-11-14 19:40
Mathlib/Analysis/RCLike/Basic.lean
feat(Analysis/InnerProductSpace/Basic): add a simp lemma (#30793) …
Added RCLike.re_ofReal_powView on Github →