faithfulSMulLeft — Mathlib

English

If M acts faithfully on α and β is nonempty, then the induced action of M on α×β is faithful in the left coordinate.

Русский

Если M действует верно на α и β непусто, то на α×β действует верно по левой координате.

LaTeX

$$$[FaithfulSMul M α]\\, [Nonempty β] \\Rightarrow FaithfulSMul M (α × β)$$$

Lean4

@[to_additive]
instance faithfulSMulLeft [FaithfulSMul M α] [Nonempty β] : FaithfulSMul M (α × β) where
  eq_of_smul_eq_smul
    h :=
    let ⟨b⟩ := ‹Nonempty β›
    eq_of_smul_eq_smul fun a : α => by injection h (a, b)

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