commute_inl_inr — Mathlib

English

The two canonical injections into the product commute: inl(m) and inr(n) satisfy inl(m) · inr(n) = inr(n) · inl(m).

Русский

Две канонические вложения в произведение commute: inl(m) и inr(n) удовлетворяют inl(m) · inr(n) = inr(n) · inl(m).

LaTeX

$$$$ inl_{\alpha,\beta}(m) \cdot inr_{\alpha,\beta}(n) = inr_{\alpha,\beta}(n) \cdot inl_{\alpha,\beta}(m). $$$$

Lean4

@[to_additive]
theorem commute_inl_inr (m : α) (n : β) : Commute (inl α β m) (inr α β n) :=
  Commute.prod (.one_right m) (.one_left n)

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