instIsMulTorsionFree — Mathlib

English

If every component M(i) is a Monoid and IsMulTorsionFree, then the Pi-type (i ↦ M(i)) is IsMulTorsionFree.

Русский

Если для каждого i модуля M(i) является моноидом и удовлетворяет свойству IsMulTorsionFree, то Pi-тип (i ↦ M(i)) также является IsMulTorsionFree.

LaTeX

$$$ \forall i, \text{IsMulTorsionFree}(M(i)) \Rightarrow \text{IsMulTorsionFree}( (i \mapsto M(i)) ) $$$

Lean4

@[to_additive]
instance instIsMulTorsionFree [∀ i, Monoid (M i)] [∀ i, IsMulTorsionFree (M i)] : IsMulTorsionFree (∀ i, M i) where
  pow_left_injective n hn a b hab := by ext i; exact pow_left_injective hn <| congr_fun hab i

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