Commit 2026-05-18 09:40 7eec3803

View on Github →

chore(Data/Nat/Cast/Order/Ring): move two Nat lemmas to Data/Nat/Basic (#38343) These two lemmas have no correlation with Nat.cast, and the proof can be golfed to fit Data/Nat/Basic.

Estimated changes

Modified Mathlib/Data/Nat/Basic.lean

added theorem Nat.mul_le_pow

added theorem Nat.two_mul_sq_add_one_le_two_pow_two_mul

Modified Mathlib/Data/Nat/Cast/Order/Ring.lean

deleted theorem Nat.mul_le_pow

deleted theorem Nat.two_mul_sq_add_one_le_two_pow_two_mul