faithfulSMulRight — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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