Skip to content

Commit

Permalink
chore: relax typeclass assumption in Polynomial.support_smul (#10397)
Browse files Browse the repository at this point in the history
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
  • Loading branch information
alreadydone and alreadydone committed Feb 10, 2024
1 parent e7a73bf commit b9ecf68
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Polynomial/Coeff.lean
Expand Up @@ -58,7 +58,7 @@ theorem coeff_smul [SMulZeroClass S R] (r : S) (p : R[X]) (n : ℕ) :
exact Finsupp.smul_apply _ _ _
#align polynomial.coeff_smul Polynomial.coeff_smul

theorem support_smul [Monoid S] [DistribMulAction S R] (r : S) (p : R[X]) :
theorem support_smul [SMulZeroClass S R] (r : S) (p : R[X]) :
support (r • p) ⊆ support p := by
intro i hi
simp? [mem_support_iff] at hi ⊢ says simp only [mem_support_iff, coeff_smul, ne_eq] at hi ⊢
Expand Down

0 comments on commit b9ecf68

Please sign in to comment.