English
Let αi be M-sets with Nonempty all αi. If at a particular index i0 the action of M on αi0 is faithful, then the coordinatewise action of M on the product ∀i αi is faithful.
Русский
Пусть для каждого i множество αi снабжено действием M. Если для некоторого индекса i0 действие M на αi0 верно-faithful, а все αi непустые, то произведение ∀i αi также обладает верным (faithful) действием M.
LaTeX
$$$\big(\exists i_0, FaithfulSMul\ M\ (\alpha_{i_0})\big) \Rightarrow FaithfulSMul\ M\big(\forall i\, \alpha_i\big).$$$
Lean4
/-- If `α i` has a faithful scalar action for a given `i`, then so does `Π i, α i`. This is
not an instance as `i` cannot be inferred. -/
@[to_additive /-- If `α i` has a faithful additive action for a given `i`, then
so does `Π i, α i`. This is not an instance as `i` cannot be inferred -/
]
theorem faithfulSMul_at [∀ i, SMul M (α i)] [∀ i, Nonempty (α i)] (i : ι) [FaithfulSMul M (α i)] :
FaithfulSMul M (∀ i, α i) where
eq_of_smul_eq_smul
h :=
eq_of_smul_eq_smul fun a : α i => by
classical simpa using congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i
