mathlib3
d33ea7b2 - chore(ring_theory/polynomial/pochhammer): make semiring implicit in a lemma that I just moved (#13077)

Commit
3 years ago
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.
Author
Parents
Loading