Theorems · Theorem · number theory
Behrend.four_zero_nine_six_lt_exp_sixteen
4096 < Real.exp 16
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- Real.logproof · cited by 939
- Real.expstatement · cited by 871
- lt_of_not_geproof · cited by 374
- neg_neg_of_posproof · cited by 227
- zero_lt_twoproof · cited by 124
- Real.rpow_natCastproof · cited by 93
- Real.log_rpowproof · cited by 31
- Nat.cast_ofNatproof · cited by 28
- Real.log_lt_iff_lt_expproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- Behrend.lower_bound_le_one'proof · cited by 1