Commit 2024-12-11 16:24 e52bfb49

View on Github →

chore(RingTheory/Binomial): make a variable implicit, misc cleanups (#19856) This PR changes the Nat variable in nsmul_right_injective to implicit. Also, the BinomialRing instance on Nat is changed to use Nat.multichoose, since (contrary to my previous impression) that function seems unlikely to be deprecated.

Estimated changes

Modified Mathlib/NumberTheory/Padics/MahlerBasis.lean

Modified Mathlib/RingTheory/Binomial.lean

modified theorem Ring.choose_smul_choose

modified theorem Ring.nsmul_right_injective