Commit 2025-06-04 02:56 5443d88c

View on Github →

feat(ContinuousFunctionalCalculus): a ^ y is invertible iff a is invertible (#25005) This PR shows that a ^ y is invertible iff a is also invertible, where the power is defined via the continuous functional calculus.

Estimated changes

added theorem CFC.isUnit_nnrpow_iff
added theorem CFC.isUnit_rpow_iff
added theorem CFC.isUnit_sqrt_iff
modified theorem CFC.rpow_add
modified theorem CFC.rpow_eq_rpow_pi
modified theorem CFC.rpow_eq_rpow_prod
added theorem CFC.rpow_inv_rpow
modified theorem CFC.rpow_map_pi
modified theorem CFC.rpow_map_prod
modified theorem CFC.rpow_mul_rpow_neg
modified theorem CFC.rpow_neg_mul_rpow
added theorem CFC.rpow_rpow_inv
modified theorem CFC.rpow_sqrt
added theorem CFC.spectrum_rpow
modified theorem CFC.sqrt_rpow
added theorem IsUnit.cfcNNRpow
added theorem IsUnit.cfcRpow
added theorem IsUnit.cfcSqrt