Commit 2024-01-08 11:01 028b9693

View on Github →

chore(Data/Nat/Choose/Multinomial): Golf (#9534) and n ! ≤ n ^ n From LeanAPAP

Estimated changes

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

added theorem Nat.multinomial_cons

modified theorem Nat.multinomial_insert

modified theorem Nat.multinomial_singleton

Modified Mathlib/Data/Nat/Factorial/Basic.lean

added theorem Nat.factorial_le_pow