instIsLeftCancelMul — Mathlib

English

If each f(i) has Mul and IsLeftCancelMul, then (i ↦ f(i)) has IsLeftCancelMul.

Русский

Если на каждом индексе i множество f(i) имеет умножение и левый отменитель, то функция (i ↦ f(i)) имеет левый отменитель.

LaTeX

$$$\\forall i, \\text{Mul}(f(i)) \\land \\forall i, \\text{IsLeftCancelMul}(f(i)) \\Rightarrow \\text{IsLeftCancelMul}(i \\mapsto f(i))$$$

Lean4

@[to_additive]
instance instIsLeftCancelMul [∀ i, Mul (f i)] [∀ i, IsLeftCancelMul (f i)] : IsLeftCancelMul (∀ i, f i) where
  mul_left_cancel _ _ _ h := funext fun _ ↦ mul_left_cancel (congr_fun h _)

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