ring — Mathlib

English

The GradeZero ring instance is constructed from the GSemiring A, with the Injections and maps preserving ring operations across the direct sum.

Русский

Рассматривается конструкция кольца GradeZero на основе GSemiring A; отображения сохраняют операции кольца в прямой сумме.

LaTeX

$$Instance Ring (A 0)$$

Lean4

/-- The `Ring` derived from `GSemiring A`. -/
instance ring : Ring (A 0) :=
  Function.Injective.ring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A) (of A 0).map_add
    (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ ↦ map_zsmul _ _ _)
    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)

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