zsmul

Mathlib.RingTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.zsmul

English

The integer scalar action zsmul is defined on Ore localization.

Русский

Целочисленное умножение zsmul определено на локализации Оре.

LaTeX

$$zsmul: Z × X[S^{-1}] → X[S^{-1}]$$

Lean4

/-- `zsmul` of `OreLocalization` -/
@[irreducible]
protected def zsmul : ℤ → X[S⁻¹] → X[S⁻¹] :=
  zsmulRec

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

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

Разделы

Аффилиация

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