support_single_mul — Mathlib

English

If G is left cancellative, the support of (single x r * f) equals the map of f.support by left embedding x.

Русский

Если левая отмена выполняется, опора (single x r) * f равна отображению опоры f левой вставкой x.

LaTeX

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

Lean4

theorem support_single_mul [IsLeftCancelMul G] (r : k) (x : G) (hrx : ∀ y, r * x • y = 0 ↔ y = 0) :
    (single x r * f : SkewMonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x) := by
  classical
  ext a
  simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]

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