Commit 2026-09-08 14:44 9a1338a6
View on Github →feat(Data/Nat/Basic): tag Nat.pow_le_pow_right with @[gcongr high] (#43505) This is maybe useful for Int too but we don't have that lemma at the moment so I'll leave that for now.
feat(Data/Nat/Basic): tag Nat.pow_le_pow_right with @[gcongr high] (#43505) This is maybe useful for Int too but we don't have that lemma at the moment so I'll leave that for now.