mul

Mathlib.Algebra.GroupWithZero.Basic

URI: https://scilib.ai/kg/mathlib#NeZero.mul

English

If a and b are nonzero, their product is nonzero.

Русский

Если a и b не нули, их произведение не равно нулю.

LaTeX

$$(a \neq 0) \land (b \neq 0) \rightarrow a b \neq 0$$

Lean4

instance mul [Zero M₀] [Mul M₀] [NoZeroDivisors M₀] {x y : M₀} [NeZero x] [NeZero y] : NeZero (x * y) :=
  ⟨mul_ne_zero out out⟩

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

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

Разделы

Аффилиация

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