dickson_one_one_comp_comm — Mathlib

English

The composition of D_1,1 with itself is commutative: D_1,1(m) ∘ D_1,1(n) = D_1,1(n) ∘ D_1,1(m).

Русский

Композиция D_1,1 с самой собой коммутирует: D_1,1(m) ∘ D_1,1(n) = D_1,1(n) ∘ D_1,1(m).

LaTeX

$$(dickson 1 (1 : R) m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m)$$

Lean4

theorem dickson_one_one_comp_comm (m n : ℕ) :
    (dickson 1 (1 : R) m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m) := by
  rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]

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