Theorem Nat.two_mul_sq_add_one_le_two_pow_two_mul

Modification history

2024-08-04 14:32
Mathlib/Data/Nat/Cast/Order/Ring.lean
feat: Real.exists_natCast_add_one_le_pow_of_one_le (#15074) …
Added Nat.two_mul_sq_add_one_le_two_pow_two_mulView on Github →