instRing — Mathlib

English

If α is as above and 𝕜 is a ring, then IncidenceAlgebra 𝕜 α is a ring.

Русский

Если выполняются условия над α и 𝕜 — кольцо, то инцидентная алгебра образует кольцо.

LaTeX

$$$$ \\operatorname{IncidenceAlgebra} 𝕜 α \\text{ is a ring.} $$$$

Lean4

instance instRing [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Ring 𝕜] : Ring (IncidenceAlgebra 𝕜 α)
    where
  __ := instSemiring
  __ := instAddGroup

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