degrees_map_of_injective — Mathlib

English

If f is injective, mapping p preserves the full degree multiset: (map f p).degrees = p.degrees.

Русский

Если отображение f инъективно, то степени образа сохраняют степени: (map f p).degrees = p.degrees.

LaTeX

$$$[\text{CommSemiring } S] (f: R \to^+_* S), \; \mathrm{degrees}(\mathrm{map}\ f\; p) = p.degrees$$$

Lean4

theorem degrees_map_of_injective [CommSemiring S] (p : MvPolynomial σ R) {f : R →+* S} (hf : Injective f) :
    (map f p).degrees = p.degrees := by simp only [degrees, MvPolynomial.support_map_of_injective _ hf]

Похожие утверждения