instRing — Mathlib

English

There is a Ring structure on α →ᵇ R obtained via pointwise operations from the ring structure on R.

Русский

Для α →ᵇ R существует кольцо, полученное путём покоцентых операций из кольца R.

LaTeX

$$$\\text{Ring} (α \\to^b R)$ with pointwise operations$$

Lean4

instance instRing : Ring (α →ᵇ R) :=
  fast_instance%DFunLike.coe_injective.ring _ coe_zero coe_one coe_add coe_mul coe_neg coe_sub
      (fun _ _ => coe_nsmul _ _) (fun _ _ => coe_zsmul _ _) (fun _ _ => coe_pow _ _) coe_natCast coe_intCast

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