instMul

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

There is a multiplicative structure on FractionalIdeal given by mul, i.e., a Mul instance defined by I * J.

Русский

Для FractionalIdeal существует умножение, задаваемое через mul: I * J.

LaTeX

$$instance : Mul (FractionalIdeal S P) := ⟨fun I J => mul I J⟩$$

Lean4

instance : Mul (FractionalIdeal S P) :=
  ⟨fun I J => mul I J⟩

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

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

Разделы

Аффилиация

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