Theorem RCLike.im_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.im_ofReal_powView on Github →