Commit 2023-11-09 15:05 4bca330d

View on Github →

feat(SpecialFunctions/Pow): add 2 more rpow_ofNat (#8281)

  • Add NNReal.rpow_ofNat and ENNReal.rpow_ofNat.
  • Add ENNReal.rpow_lt_top_iff_of_pos.

Estimated changes

added theorem ENNReal.rpow_ofNat
modified theorem ENNReal.rpow_two
added theorem NNReal.rpow_ofNat
modified theorem NNReal.rpow_two