instHasQuotient — Mathlib

English

The quotient R/I is defined as the corresponding submodule quotient, i.e., the quotient by I regarded as a submodule of R.

Русский

Фактор-кольцо R/I определяется как соответствующая фактор по подмодулю I в R.

LaTeX

$$HasQuotient R (Ideal R)$$

Lean4

/-- The quotient `R/I` of a ring `R` by an ideal `I`,
defined to equal the quotient of `I` as an `R`-submodule of `R`. -/
instance instHasQuotient : HasQuotient R (Ideal R) :=
  Submodule.hasQuotient

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