zero_qsmul

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.zero_qsmul

English

0 acts as the zero scalar: 0 • x = 0 for any x in DivisibleHull M.

Русский

Нулевой скаляр действует тождественно: $0 \\cdot x = 0$ для любого $x$.

LaTeX

$$$0\\cdot x = 0$$$

Lean4

theorem zero_qsmul (x : DivisibleHull M) : (0 : ℚ) • x = 0 := by simp [qsmul_def]

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

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

Разделы

Аффилиация

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