prod_unique — Mathlib

English

If f: R →+* S × T is a ring homomorphism, then ((fst ∘ f) × (snd ∘ f)) = f; i.e., f is determined by its two coordinate maps.

Русский

Если f: R →+* S × T — гомоморфизм, то ((fst ∘ f) × (snd ∘ f)) = f; то есть f задаётся двумя координатами.

LaTeX

$$$ ((\\text{fst} \\circ f) \\times (\\text{snd} \\circ f)) = f. $$$

Lean4

theorem prod_unique (f : R →+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

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