Theorem Polynomial.add_eq_add

Modification history

2025-12-17 09:29
Mathlib/Algebra/Polynomial/Basic.lean
feat: avoid `private irreducible_def` using module system (#32861) …
Deleted Polynomial.add_eq_addView on Github →
2024-04-16 11:34
Mathlib/Algebra/Polynomial/Basic.lean
chore: backports from #11997, adaptations for nightly-2024-04-07 (#12176) …
Added Polynomial.add_eq_addView on Github →