commute_inlₗ_inrₗ — Mathlib

English

In the lexicographic setting, inlₗ(m) and inrₗ(n) commute: inlₗ(m) · inrₗ(n) = inrₗ(n) · inlₗ(m).

Русский

В лексикографическом порядке inlₗ(m) и inrₗ(n) commute: inlₗ(m) · inrₗ(n) = inrₗ(n) · inlₗ(m).

LaTeX

$$$$ inl_{\ell}(m) \cdot inr_{\ell}(n) = inr_{\ell}(n) \cdot inl_{\ell}(m). $$$$

Lean4

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

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