instRing — Mathlib

English

If β is a Ring, then SimpleFunc α β inherits a Ring structure via pointwise operations.

Русский

Если β — кольцо, то SimpleFunc α β получает структуру кольца по точкам.

LaTeX

$$$\\text{instRing }[Ring\\ \\beta] : Ring (\\alpha \\to_{S} \\beta).$$$

Lean4

instance [Ring β] : Ring (α →ₛ β) :=
  fast_instance%Function.Injective.ring (fun f => show α → β from f) coe_injective coe_zero coe_one coe_add coe_mul
      coe_neg coe_sub coe_smul coe_smul coe_pow coe_natCast coe_intCast

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