IsCycle₂ — Mathlib

English

For any g ∈ G and a ∈ A, IsCycle₁ of the singleton g acting on a holds exactly when g fixes a.

Русский

Для любого g ∈ G и элемента a ∈ A условие IsCycle₁ для одинокого элемента g·a выполняется тогда и только тогда, когда g фиксирует a.

LaTeX

$$$IsCycle_1 (single\; g\; a) \;\iff\; g \cdot a = a$$$

Lean4

/-- A finsupp `∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A` satisfies the 2-cycle condition if
`∑ (gᵢ⁻¹ • aᵢ)·hᵢ + aᵢ·gᵢ = ∑ aᵢ·gᵢhᵢ`. -/
def IsCycle₂ (x : G × G →₀ A) : Prop :=
  x.sum (fun g a => single g.2 (g.1⁻¹ • a) + single g.1 a) = x.sum (fun g a => single (g.1 * g.2) a)

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