cyclesOfIsCycle₂ — Mathlib

English

There is an equivalence between IsCycle₂ for a general pair g and the sum identity on its components after projecting and combining via multiplication.

Русский

Существует эквивалентность IsCycle₂ для пары g и суммы после проекции и комбинирования через умножение.

LaTeX

$$$IsCycle_2 (Finsupp.single\; g\ a) \iff (g.snd\; a) + (g.fst\; (g.fst \cdot a)) = (g.fst g.snd) a$$$

Lean4

/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G × G →₀ A` satisfying the 2-cycle condition, produces a 2-cycle for the representation on
`A` induced by the `DistribMulAction`. -/
@[simps]
def cyclesOfIsCycle₂ (x : G × G →₀ A) (hx : IsCycle₂ x) : cycles₂ (Rep.ofDistribMulAction k G A) :=
  ⟨x, (mem_cycles₂_iff (A := Rep.ofDistribMulAction k G A) x).2 hx⟩

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