prod_top — Mathlib

English

The product with top on the second factor equals the subsemiring obtained by pulling back along fst.

Русский

Произведение с верхом по второй компоненте равно подполем, полученному тянущей по fst.

LaTeX

$$$ s.prod (\\top : NonUnitalSubsemiring S) = s.comap (NonUnitalRingHom.fst R S) $$$

Lean4

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

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