fst_comp_coe_prodComm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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