support_single_mul — Mathlib

English

For a monoid with 1, the support of the unit element is contained in {1}.

Русский

Для моноида с единицей опора единицы содержится в {1}.

LaTeX

$$(Supp(1)) ⊆ 1$$

Lean4

theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0)
    (x : G) : (single x r * f : MonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x) := by
  classical
  ext
  simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image, mem_map, mulLeftEmbedding_apply]

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