English
Let e_i : R_i ≃+* S_i and f_i : S_i ≃+* T_i be ring isomorphisms for every index i in some index type ι. Then the composed right pi-congruence equals the pi-congruence of the pointwise compositions: (πCongrRight e).trans (πCongrRight f) = πCongrRight (λ i, (e i).trans (f i)).
Русский
Пусть для каждого индекса i из множества ι заданы кольцевые эквивалентности e_i: R_i ≃+* S_i и f_i: S_i ≃+* T_i. Тогда композиция по координатному конгруентному переносу справа равна конгруентности по точному произведению композиций: (πCongrRight e).trans (πCongrRight f) = πCongrRight (λ i, (e i).trans (f i)).
LaTeX
$$$$\\ (\\pi\\text{-CongrRight } e).\\text{trans}(\\pi\\text{-CongrRight } f) \;=\\; \\pi\\text{-CongrRight} \\Big( \\lambda i, (e i).\\text{trans}(f i) \\Big) \\;.$$$$
Lean4
@[simp]
theorem piCongrRight_trans {ι : Type*} {R S T : ι → Type*} [∀ i, NonUnitalNonAssocSemiring (R i)]
[∀ i, NonUnitalNonAssocSemiring (S i)] [∀ i, NonUnitalNonAssocSemiring (T i)] (e : ∀ i, R i ≃+* S i)
(f : ∀ i, S i ≃+* T i) : (piCongrRight e).trans (piCongrRight f) = piCongrRight fun i => (e i).trans (f i) :=
rfl
