Commit 2026-02-16 14:47 d0d33f98

View on Github →

chore(NumberTheory/Height/Basic): fix names, add to_fun, more API (#35407) This PR does some house-keeping:

  • change two names from zero_le_xxx to xxx_nonneg as per the naming convention
  • add to_fun to mulHeight_{zero|one}
  • add the two parallel API lemmas logHeight_{zero|one} (with to_fun attribute)

Estimated changes

added theorem Height.logHeight_one
added theorem Height.logHeight_zero
deleted theorem Height.mulHeight.ne_zero
deleted theorem Height.zero_le_logHeight