ModP — Mathlib

English

For a commutative ring O and natural p, ModP O p denotes the quotient of O by the ideal generated by p, i.e., O/(p).

Русский

Для коммутативного кольца O и натурального p модуль ModP O p обозначает факторкольцо O/(p), где (p) — порождённый p идеал.

LaTeX

$$$\mathrm{ModP}(O,p) = O / (p)$$$

Lean4

/-- `O/(p)` for `O`, ring of integers of `K`. -/
def ModP :=
  O ⧸ (Ideal.span {(p : O)} : Ideal O)

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