some_mul_some

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.some_mul_some

English

Some(a) * Some(b) = Some(a * b) when multiplication is defined.

Русский

Some(a) * Some(b) = Some(a * b), когда умножение определено.

LaTeX

$$$ \operatorname{Some}(a) * \operatorname{Some}(b) = \operatorname{Some}(a * b) $$$

Lean4

@[to_additive]
theorem some_mul_some [Mul α] (a b : α) : some a * some b = some (a * b) := by simp [mul_def]

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

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

Разделы

Аффилиация

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