Commit 2026-05-01 05:59 5198248e

View on Github →

feat(Algebra/MvPolynomial/Variables): add some lemmas about vars (#37791) These lemmas are used in #36103

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Monad.lean

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

deleted theorem MvPolynomial.mem_vars

added theorem MvPolynomial.mem_vars_iff_degreeOf_ne_zero

added theorem MvPolynomial.mem_vars_iff_mem_support

added theorem MvPolynomial.support_subset_vars_of_mem_support

added theorem MvPolynomial.vars_eq_empty_iff_eq_C

Modified Mathlib/FieldTheory/SeparablyGenerated.lean

Modified Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean