FaithfulSMul' — Mathlib

English

For a fixed i, if the M-action on α_i is faithful, then the M-action on the Σ-type Σ i, α_i is faithful as well.

Русский

Для фиксированного i, если действие M на α_i верно, то действие M на Σ i, α_i тоже верно.

LaTeX

$$$[\forall i, FaithfulSMul M (α_i)] \Rightarrow FaithfulSMul M (\Sigma i, α_i).$$$

Lean4

/-- This is not an instance because `i` becomes a metavariable. -/
@[to_additive /-- This is not an instance because `i` becomes a metavariable. -/
    ]
protected theorem FaithfulSMul' [FaithfulSMul M (α i)] : FaithfulSMul M (Σ i, α i) :=
  ⟨fun h => eq_of_smul_eq_smul fun a : α i => heq_iff_eq.1 (Sigma.ext_iff.1 <| h <| mk i a).2⟩

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