Theorem Submultiplicative.eventually_rpow_lt_of_rpow_lt

Modification history

2026-09-30 08:09
Mathlib/Analysis/Subadditive.lean
feat(Analysis/Subadditive): multiplicative Fekete's lemma (#42605) …
Added Submultiplicative.eventually_rpow_lt_of_rpow_ltView on Github →