isCycle₁_of_mem_cycles₁ — Mathlib

English

A two-cycle condition for a singleton is equivalent to a sum identity on the two projections.

Русский

Условие 2-цикла для одиночного элемента эквивалентно суммному тождеству по двум проекциям.

LaTeX

$$$IsCycle_2 (single g a) \iff (\text{sum of projections}) = (single (g_1 g_2) (g_1 \cdot a))$$$

Lean4

theorem isCycle₁_of_mem_cycles₁ (x : G →₀ A) (hx : x ∈ cycles₁ (Rep.ofDistribMulAction k G A)) : IsCycle₁ x := by
  simpa using (mem_cycles₁_iff (A := Rep.ofDistribMulAction k G A) x).1 hx

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