snd_comp_coe_prodComm — Mathlib

English

The composition of RingHom.snd with the coerced prodComm equals RingHom.fst: snd ∘ ↑prodComm = fst.

Русский

Составление RingHom.snd с вложенным prodComm равно RingHom.fst: snd ∘ ↑prodComm = fst.

LaTeX

$$$ (\\text{RingHom.snd } S R) \\circ ↑(\\text{prodComm } R S) = \\text{RingHom.fst } R S. $$$

Lean4

@[simp]
theorem snd_comp_coe_prodComm : (RingHom.snd S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.fst R S :=
  RingHom.ext fun _ => rfl

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