support_mul_single — Mathlib

English

If f ∈ MonoidAlgebra and r ∈ k with a suitable hr, then the support of f * single x r equals the mapped support via the right embedding.

Русский

Если f ∈ MonoidAlgebra и r ∈ k при подходящем hr, то опора f * single x r равна образу опоры через правое вложение.

LaTeX

$$Supp( f * single x r ) = map (mulRightEmbedding x) f.support$$

Lean4

theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0)
    (x : G) : (f * single x r).support = f.support.map (mulRightEmbedding x) := by
  classical
  ext
  simp only [support_mul_single_eq_image f hr (IsRightRegular.all x), mem_image, mem_map, mulRightEmbedding_apply]

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