instNoZeroDivisors

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.instNoZeroDivisors

English

Constant multiplication distributes over multiplication of constants: (C a) * (C a') = C (a a').

Русский

Константное умножение распределяется по умножению констант: (C a) * (C a') = C (a a').

LaTeX

$$$ (C\ a) * (C\ a') = C\ (a * a') $$$

Lean4

instance [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (MvPolynomial σ R) :=
  inferInstanceAs (NoZeroDivisors (AddMonoidAlgebra ..))

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

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

Разделы

Аффилиация

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