Theorem MonomialOrder.degree_of_subsingleton

Modification history

2026-08-17 20:58

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

chore(RingTheory/MvPolynomial/MonomialOrder): rename `degree_subsingleton` to `degree_of_subsingleton` (#42853) …

Added MonomialOrder.degree_of_subsingleton View on Github →