instFaithfulSMulForallOfNontrivial

English

If M acts faithfully on α and on α → β under Nontrivial β, then the induced action on α → β is faithful; i.e., eq_of_smul_eq_smul holds only for equal scalars.

Русский

Если M действует достоверно на α и на α → β при не тривиальном β, то индуцированное действие на α → β достоверно; равенство скалярных действий на все функции эквивалентно равенству самих скаляров.

LaTeX

$$$\text{FaithfulSMul } M^{\mathrm{dm}} (\alpha \to \beta)$$$

Lean4

@[to_additive]
instance [SMul M α] [FaithfulSMul M α] [Nontrivial β] : FaithfulSMul Mᵈᵐᵃ (α → β) where
  eq_of_smul_eq_smul {c₁ c₂}
    h :=
    mk.symm.injective <|
      eq_of_smul_eq_smul fun a : α ↦ by
        rcases exists_pair_ne β with ⟨x, y, hne⟩
        contrapose! hne
        haveI := Classical.decEq α
        replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
        simpa [smul_apply, hne] using h

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