Commit 2024-11-28 15:29 74671447
View on Github →refactor(Algebra/Polynomial/Laurent): simplify some proofs (#19534)
This PR simplifies a few proofs about Laurent polynomials and adds the trivial theorem Polynomial.toLaurent_eq_zero. It also changes the type of Lauren.isLocalization to use Submonoid.powers instead of Submonoid.closure, which I think is the more natural thing to do here.