Commit 2025-09-16 11:11 d98f0bbf
View on Github →feat(Analysis/SpecialFunctions/CFC/Rpow): 0 ≤ a iff a = star b * b for some b (#29592)
It can sometimes be convenient to directly have this form for non-negative elements.
feat(Analysis/SpecialFunctions/CFC/Rpow): 0 ≤ a iff a = star b * b for some b (#29592)
It can sometimes be convenient to directly have this form for non-negative elements.