support_mul_single — Mathlib

English

In a cancellative monoid, the support of (f * single x r) equals the map of f.support by multiplication by x.

Русский

В квазиклассном моноиде опора f * single x r равна отображению опоры f умножением на x.

LaTeX

$$(f * single x r).\\operatorname{support} = \\operatorname{map} (mulRightEmbedding x)\\ f.\\operatorname{support}$$

Lean4

theorem support_mul_single [IsRightCancelMul G] (r : k) (x : G) (hrx : ∀ g : G, ∀ y, y * g • r = 0 ↔ y = 0) :
    (f * single x r).support = f.support.map (mulRightEmbedding x) := by
  classical
  ext a
  simp [support_mul_single_eq_image f (IsRightRegular.all x) hrx]

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