instSemiringQuotient — Mathlib

English

The quotient c.Quotient carries a semiring structure.

Русский

У фактор-группы Quotient есть структура полуринга (полугруппы с аддитивной структурой).

LaTeX

$$$$ c.Quotient \text{ is a Semiring. } $$$$

Lean4

instance [Semiring R] (c : RingCon R) : Semiring c.Quotient :=
  fast_instance%Function.Surjective.semiring _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl) (fun _ _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl

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