instIsCancelMul

Mathlib.Algebra.Group.Pi.Basic

URI: https://scilib.ai/kg/mathlib#Pi.instIsCancelMul

English

If every f(i) has IsCancelMul, then the Pi-type (i ↦ f(i)) has IsCancelMul.

Русский

Если каждый f(i) имеет IsCancelMul, то Pi-тип (i ↦ f(i)) имеет IsCancelMul.

LaTeX

$$$\\forall i, \\text{IsCancelMul}(f(i)) \\Rightarrow \\text{IsCancelMul}(i \\mapsto f(i))$$$

Lean4

@[to_additive]
instance instIsCancelMul [∀ i, Mul (f i)] [∀ i, IsCancelMul (f i)] : IsCancelMul (∀ i, f i) where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru