mathlib

94a20a74 - chore(data/polynomial/degree/definitions): make an argument explicit (#15951)

chore(data/polynomial/degree/definitions): make an argument explicit (#15951) The argument `n : ℕ` cannot be deduced from the goal and it is useful to be able to provide it. This argument changed from explicit to implicit when I prepared #15818.