How to formalize (3x - 2y)¹⁸ Expansion Coefficient?

Stream: maths

[Jasin Jiang]

Hello! I want wo formalize the exercies:

What is the coefficient of x^5y^13 in the expansion of (3x - 2y)^18?

I'm not quite sure if I've formalized this correctly, or if there are better, more concise formalization methods?

import Mathlib

open MvPolynomial Finset Nat

def x_idx : Fin 2 := 0
def y_idx : Fin 2 := 1

noncomputable def P : MvPolynomial (Fin 2) ℤ := (3 * (X x_idx) - 2 * (X y_idx)) ^ 18

noncomputable def monomial_exponents : Fin 2 →₀ ℕ :=
  (Finsupp.single x_idx 5) + (Finsupp.single y_idx 13)

example :
  MvPolynomial.coeff monomial_exponents P = (Nat.choose 18 5) * (3 : ℤ) ^ 5 * (-2 : ℤ) ^ 13 := by
  sorry

[Ruben Van de Velde]

That looks like it'd work, yeah. You could declare a custom type rather than Fin 2, but not sure if that would end up better or worse

[Kenny Lau]

After #28349 Fin 2 would be highly preferred.

[Jasin Jiang]

Ruben Van de Velde said:

That looks like it'd work, yeah. You could declare a custom type rather than Fin 2, but not sure if that would end up better or worse

Well now I'm trying to prove it.

[Riccardo Brasca]

We surely know that monomials form a basis of the polynomials, so, given the monomial, the "coefficient function" is already there

[Kenny Lau]

@Riccardo Brasca that's already the approach taken in the code above

[Jasin Jiang]

Kenny Lau said:

that's already the approach taken in the code above

Yesterday I tried to complete this sorry proof, and I found it a bit difficult. Do you have any experience with this kind of proof?

[Kenny Lau]

@Jasin Jiang the trick is to distribute coeff linearly even though it's zero elsewhere, i.e. coeff x^2 (1+x+x^2+x^4) = coeff x^2 1 + coeff x^2 x + coeff x^2 x^2 + coeff x^2 x^4 = 0 + 0 + 1 + 0 = 1