isCycle₂_of_mem_cycles₂ — Mathlib

English

If x belongs to the cycles₂ subgroup of Rep.ofDistribMulAction, then x is a 2-cycle.

Русский

Если x принадлежит подгруппе cycles₂ Rep.ofDistribMulAction, тогда x является 2-циклом.

LaTeX

$$$x \in cycles_2 (Rep.ofDistribMulAction k G A) \Rightarrow IsCycle_2 x$$$

Lean4

theorem isCycle₂_of_mem_cycles₂ (x : G × G →₀ A) (hx : x ∈ cycles₂ (Rep.ofDistribMulAction k G A)) : IsCycle₂ x :=
  (mem_cycles₂_iff (A := Rep.ofDistribMulAction k G A) x).1 hx

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