instRing — Mathlib

English

If Y is a ring, LocallyConstant(X, Y) becomes a ring with operations defined pointwise.

Русский

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

LaTeX

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

Lean4

instance [Ring Y] : Ring (LocallyConstant X Y) :=
  Function.Injective.ring 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

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