abs_qsmul

Mathlib.Algebra.Order.Module.Rat

URI: https://scilib.ai/kg/mathlib#abs_qsmul

← MathLib Explorer

English

For q ∈ ℚ and a ∈ α, |q a| = |q| |a| under appropriate order and action assumptions.

Русский

Для q ∈ ℚ и a ∈ α выполняется |qa| = |q| |a| при условии порядка и действия.

LaTeX

$$$|q\\cdot a| = |q|\\cdot|a|$$$

Lean4

@[deprecated abs_smul (since := "2025-06-24")]
theorem abs_qsmul [Module ℚ α] [PosSMulMono ℚ α] (q : ℚ) (a : α) : |q • a| = |q| • |a| :=
  abs_smul q a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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