Commit 2024-06-24 16:56 aa881f56

View on Github →

feat(Algebra/Order/Ring/WithTop): add generalised and specialised power of top (#14019)

  • Add generalised version of top_pow in Algebra/Order/Ring/WithTop
  • Add specialised version of top_pow in Data/ENat/Basic.lean
  • Add specialised version of top_pow in Data/ENNReal/Operations.lean Co-authored by @D-Thomine.

Estimated changes

added theorem WithTop.top_pow
modified theorem ENNReal.top_pow
added theorem ENat.top_pow