snd_mul — Mathlib

English

For all p, q in M × N, the second coordinate of the product equals the product of the second coordinates: (p · q).2 = p.2 · q.2.

Русский

Для любых p, q ∈ M × N вторая координата произведения равна произведению вторых координат: (p · q)2 = p2 · q2.

LaTeX

$$$\forall p,q \in M \times N,\ (p q)_2 = p_2 q_2$$$

Lean4

@[to_additive (attr := simp)]
theorem snd_mul (p q : M × N) : (p * q).2 = p.2 * q.2 :=
  rfl

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