mul

Mathlib.Topology.Algebra.Monoid

URI: https://scilib.ai/kg/mathlib#Inseparable.mul

English

If a is inseparable from b and c inseparable from d, then a·c is inseparable from b·d.

Русский

Если ainseparable a и b, и c inseparable от d, то a·c inseparable от b·d.

LaTeX

$$$\text{Inseparable}(a,c) \land \text{Inseparable}(b,d) \Rightarrow \text{Inseparable}(a c, b d)$$$

Lean4

@[to_additive]
protected theorem mul {a b c d : M} (hab : Inseparable a b) (hcd : Inseparable c d) : Inseparable (a * c) (b * d) :=
  hab.smul hcd

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

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

Разделы

Аффилиация

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