elimMonom — Mathlib

Lean4
/-- `elimMonom s map` eliminates the monomial level of the `Sum` `s`.

`map` is a lookup map from monomials to variable numbers.
The output `TreeMap ℕ ℤ` has the same structure as `s : Sum`,
but each monomial key is replaced with its index according to `map`.
If any new monomials are encountered, they are assigned variable numbers and `map` is updated.
-/
def elimMonom (s : Sum) (m : Map Monom ℕ) : Map Monom ℕ × Map ℕ ℤ :=
  s.foldr
    (fun mn coeff ⟨map, out⟩ ↦
      match map[mn]? with
      | some n => ⟨map, out.insert n coeff⟩
      | none =>
        let n := map.size
        ⟨map.insert mn n, out.insert n coeff⟩)
    (m, TreeMap.empty)
Похожие утверждения