abv_mul

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#IsAbsoluteValue.abv_mul

English

abv(xy) = abv(x) abv(y).

Русский

abv(xy) = abv(x) abv(y).

LaTeX

$$$\\operatorname{abv}(xy) = \\operatorname{abv}(x) \\operatorname{abv}(y)$$$

Lean4

theorem abv_mul (x y) : abv (x * y) = abv x * abv y :=
  abv_mul' x y

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

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

Разделы

Аффилиация

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