instInfiniteProdSubtypeCommute — Mathlib

English

If α is an infinite group, the set of pairs (p1,p2) with p1 and p2 commuting is infinite.

Русский

Если α бесконечна, множество пар (p1,p2), которые коммутируют, бесконечно.

LaTeX

$$$\text{Infinite} \{ p:\alpha\times\alpha\mid \operatorname{Commute}(p.1,p.2) \}$$$

Lean4

instance instInfiniteProdSubtypeCommute [Mul α] [Infinite α] : Infinite { p : α × α // Commute p.1 p.2 } :=
  Infinite.of_injective (fun a => ⟨⟨a, a⟩, rfl⟩) (by intro; simp)

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