basic): fix unexpected change of an implicit parameter (#13935)

Commit

3 years ago

fix(ring_theory/polynomial/basic): fix unexpected change of an implicit parameter (#13935) Fix unexpected change of an implicit parameter in the previous PR(#13800). Fix docstring.

Author

astrainfinita

Parents

53c79d56

mathlib ceca8d74 - fix(ring_theory/polynomial/basic): fix unexpected change of an implicit parameter (#13935)

mathlib
ceca8d74 - fix(ring_theory/polynomial/basic): fix unexpected change of an implicit parameter (#13935)