instNatCastCoeOfAddSubmonoidWithOneClass

English

There is a natural-number casting map into the restricted product; the image of n acts as coordinatewise n-times addition, given AddSubmonoidWithOne structure on fibers.

Русский

Существует отображение натуральных чисел в ограниченное произведение, переводящее n в по координатам n раз сложение внутри волокон.

LaTeX

$$$ n \mapsto (n, n, \dots) $ (coordinatewise via fiberwise addition). $$$

Lean4

instance [Π i, AddMonoidWithOne (R i)] [∀ i, AddSubmonoidWithOneClass (S i) (R i)] : NatCast (Πʳ i, [R i, B i]_[𝓕])
    where natCast n := ⟨fun _ ↦ n, .of_forall fun _ ↦ natCast_mem _ n⟩

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