English
If for each i, f(i) is a Mul and IsLeftCancelMul, then the Pi-type ∀i f(i) is IsLeftCancelMul.
Русский
Если для каждого i выполнено, что f(i) — мульт, и что f(i) обладает свойством левого отменителя, то ∀i f(i) обладает этим свойством.
LaTeX
$$$\\forall i,\\, \\text{Mul}(f(i)) \\land \\forall i,\\, \\text{IsLeftCancelMul}(f(i)) \\Rightarrow \\text{IsLeftCancelMul}(\\forall i, f(i))$$$
Lean4
@[to_additive]
instance monoid [∀ i, Monoid (f i)] : Monoid (∀ i, f i)
where
__ := semigroup
__ := mulOneClass
npow := fun n x i => x i ^ n
npow_zero := by intros; ext; exact Monoid.npow_zero _
npow_succ := by intros; ext; exact Monoid.npow_succ _ _
