Commit 2025-10-20 08:46 57a8e09f

View on Github →

chore(Analysis/SpecialFunctions/Log/PosLog): golf a proof using grw (#30704)

Estimated changes

added theorem Real.posLog_le_posLog