instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset

English

There is a canonical FunLike structure on the Basis g, giving a function-like interpretation of basis elements on cycle-factors Finset.

Русский

Существует каноническая структура FunLike на Basis g, дающая функциональное представление элементов базиса на Finset факторов цикла.

LaTeX

$$$\text{Basis}(g) \;\text{has a natural} \; \text{FunLike structure on } g.cycleFactorsFinset$$$

Lean4

instance (g : Perm α) : FunLike (Basis g) g.cycleFactorsFinset α
    where
  coe a := a.toFun
  coe_injective' a a' _ := by cases a; cases a'; congr

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