English
A second instance of the map-on-of compatibility: map f applied to the i-th summand equals the i-th mapped summand.
Русский
Еще одно утверждение совместимости map с виджетом of: map f (of i x) = of i (f_i x).
LaTeX
$$$$\\mathrm{map}\\; f\\; (\\mathrm{DirectSum.of}\\; \\alpha\\; i\\; x) = \\mathrm{DirectSum.of}\\; \\beta\\; i\\; (f_i\\; x).$$$$
Lean4
/-- The `Ring` derived from `GSemiring A`. -/
instance ring : Ring (⨁ i, A i) :=
{ DirectSum.semiring A,
(inferInstance :
AddCommGroup (⨁ i, A i)) with
toIntCast.intCast := fun z => of A 0 <| (GRing.intCast z)
intCast_ofNat := fun _ => congrArg (of A 0) <| GRing.intCast_ofNat _
intCast_negSucc := fun _ => (congrArg (of A 0) <| GRing.intCast_negSucc_ofNat _).trans <| map_neg _ _ }
