instFaithfulSMul — Mathlib

English

If the scalar action is faithful, SkewMonoidAlgebra k G is a faithful S-module; equality of actions implies equality of elements.

Русский

Если действие скаляра является достоверным (faithful), SkewMonoidAlgebra k G является достоверным S-модулем; совпадение действий влечёт равенство элементов.

LaTeX

$$$ \text{FaithfulSMul } S (SkewMonoidAlgebra k G) $$$

Lean4

instance instFaithfulSMul [AddMonoid k] [SMulZeroClass S k] [FaithfulSMul S k] [Nonempty G] :
    FaithfulSMul S (SkewMonoidAlgebra k G) where
  eq_of_smul_eq_smul {_s₁ _s₂}
    h := by
    apply eq_of_smul_eq_smul fun a : G →₀ k ↦ congr_arg toFinsupp _
    intro a
    simp_rw [ofFinsupp_smul, h]

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