map_mul

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.map_mul

English

For all x,y, abv(x*y) = abv(x) * abv(y).

Русский

Для любых x,y выполняется abv(xy) = abv(x)abv(y).

LaTeX

$$$\forall x,y:\ abv(x\cdot y)=abv(x)\cdot abv(y)$$$

Lean4

@[simp]
protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y :=
  abv.map_mul' x y

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

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

Разделы

Аффилиация

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