Theorem Nat.factorial_le_of_le

Modification history

2023-11-17 11:02

Mathlib/Data/Nat/Factorial/Basic.lean

fix: some cleanup in `Nat.Factorial.Basic` (#8422) …

Deleted Nat.factorial_le_of_le View on Github →

2023-06-21 09:25

Mathlib/Data/Nat/Factorial/Basic.lean

feat: golf IMO 2019 q4 (#5310) …

Added Nat.factorial_le_of_le View on Github →