coe_prod — Mathlib

English

The product subsemigroup S.prod T has a carrier equal to the product of the carriers of S and T.

Русский

Подполугруппа S.prod T имеет множество элементов, равное произведению множеств S и T.

LaTeX

$$$(S.prod T : Set (M\\times N)) = (S : Set M) \\timesˢ (T : Set N)$$$

Lean4

@[to_additive (attr := norm_cast) coe_prod]
theorem coe_prod (s : Subsemigroup M) (t : Subsemigroup N) : (s.prod t : Set (M × N)) = (s : Set M) ×ˢ (t : Set N) :=
  rfl

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