Commit 2025-01-10 13:20 b1178f18

View on Github →

feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) This adds a few lemmas on powers with real exponents:

  • injectivity as a function of the exponent (when the base is positive and ≠ 1)
  • (x ^ y) ^ n = (x ^ n) ^ y when y is real and n is a natural number or an integer

Estimated changes

added theorem Real.rpow_pow_comm
added theorem Real.rpow_right_inj
added theorem Real.rpow_zpow_comm