instIsRightCancelMul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance instIsRightCancelMul [∀ i, Mul (f i)] [∀ i, IsRightCancelMul (f i)] : IsRightCancelMul (∀ i, f i) where
  mul_right_cancel _ _ _ h := funext fun _ ↦ mul_right_cancel (congr_fun h _)

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