instCommRing — Mathlib

English

If Y is a commutative ring, LocallyConstant(X, Y) inherits a commutative ring structure with pointwise operations.

Русский

Если Y — коммутативное кольцо, LocallyConstant(X, Y) наследует коммутативное кольцо с точечно определяемыми операциями.

LaTeX

$$$\operatorname{CommRing}(\operatorname{LocallyConstant}(X,Y))$$$

Lean4

instance [CommRing Y] : CommRing (LocallyConstant X Y) :=
  Function.Injective.commRing DFunLike.coe DFunLike.coe_injective' rfl rfl (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl

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