faithfulSMul — Mathlib

English

If every αi carries a faithful SMul M-action, then the Pi-type ∀i αi carries a faithful SMul M-action.

Русский

Если на каждом αi имеется верное (faithful) действие скаляров M, то на произведении ∀i αi действует верное действие M.

LaTeX

$$$FaithfulSMul\ M\big(\forall i\, \alpha_i\big).$$$

Lean4

@[to_additive]
instance faithfulSMul [Nonempty ι] [∀ i, SMul M (α i)] [∀ i, Nonempty (α i)] [∀ i, FaithfulSMul M (α i)] :
    FaithfulSMul M (∀ i, α i) :=
  let ⟨i⟩ := ‹Nonempty ι›
  faithfulSMul_at i

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