instMul

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.instMul

English

Multiplication in the quotient is induced by multiplication in the base ring: the product of classes is the class of the product.

Русский

Умножение в кольце-остатке задаётся образами умножения в исходном кольце: произведение классов равно классу произведения.

LaTeX

$$$[a] \cdot [b] = [ab]$$$

Lean4

instance : Mul (RingQuot r) :=
  ⟨mul r⟩

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

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

Разделы

Аффилиация

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