Commit 2022-04-03 04:50 d33ea7b2

chore(ring_theory/polynomial/pochhammer): make semiring implicit in a lemma that I just moved (#13077) Moving lemma pochhammer_succ_eval to reduce typeclass assumptions (#13024), the semiring became accidentally explicit. Since one of the explicit arguments of the lemma is a term in the semiring, I changed the semiring to being implicit. The neighbouring lemmas do not involve terms in their respective semiring, which is why the semiring is explicit throughout the section.