Commit 2024-01-16 23:32 a316e2b3

View on Github →

chore(ENat/Basic): review (#9787)

  • Add ENat.mul_top and ENat.top_mul.
  • Remove some newlines.
  • Rename assumptions in ENat.recTopCoe.

Estimated changes

added theorem ENat.mul_top
modified def ENat.recTopCoe
modified def ENat.toNat
added theorem ENat.top_mul