Commit 2025-07-02 18:41 4c279ebc
View on Github →feat: version of prod_range_induction with weaker assumptions (#26570)
prod_range_induction currently requires ratios of adjacent terms to be checked for the entire sequence, but we only need to check terms up to n. I relax this assumption in prod_range_induction.