single_isCycle₁_of_mem_fixedPoints

English

If x lies in cycles₁(Rep.ofDistribMulAction), then x is a cycle in the representation.

Русский

Если x лежит в cycles₁(Rep.ofDistribMulAction), то x является циклом в представлении.

LaTeX

$$$x \in cycles_1(Rep.ofDistribMulAction\; k\; G\; A) \Rightarrow IsCycle_1(x)$$$

Lean4

theorem single_isCycle₁_of_mem_fixedPoints (g : G) (a : A) (ha : a ∈ MulAction.fixedPoints G A) :
    IsCycle₁ (single g a) := by simp_all [IsCycle₁]

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