prod_top — Mathlib

English

For any subsemiring s of R, the product s.prod ⊤ (with the top subsemiring of S) equals the comap of s along the first projection fst: s.prod ⊤ = s.comap (fst : R × S → R).

Русский

Для подполусемиринга s ⊆ R верно: s.prod ⊤ = s.comap (fst : R × S → R).

LaTeX

$$$s.prod(\\top) = s. comap(\\text{RingHom.fst } R S)$$$

Lean4

theorem prod_top (s : Subsemiring R) : s.prod (⊤ : Subsemiring S) = s.comap (RingHom.fst R S) :=
  ext fun x => by simp [mem_prod]

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