top_prod — Mathlib

English

The top element on the left product with s corresponds to pulling back along snd.

Русский

Верхний элемент слева в произведении с s соответствует вытягиванию по snd.

LaTeX

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

Lean4

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

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