single_isCycle₂_iff_inv — Mathlib

English

For any g ∈ G×G and a ∈ A, IsCycle₂(single g a) is equivalent to the equality single g.2 (g.1⁻¹ • a) + single g.1 a = single (g.1 * g.2) a.

Русский

Для любых g ∈ G×G и a ∈ A равносильно IsCycle₂(одиночный g a) равенства: single g.2 (g.1⁻¹ • a) + single g.1 a = single (g.1 * g.2) a.

LaTeX

$$$IsCycle_2 (single\; g\, a) \iff single\; g.2 (g.1^{-1} \cdot a) + single\; g.1 a = single\; (g.1 g.2) a$$$

Lean4

theorem single_isCycle₂_iff_inv (g : G × G) (a : A) :
    IsCycle₂ (single g a) ↔ single g.2 (g.1⁻¹ • a) + single g.1 a = single (g.1 * g.2) a := by simp [IsCycle₂]

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