instFintype — Mathlib

English

For finitely many α, β with Mul, the type α ≃* β of multiplicative equivalences is finite.

Русский

Для конечно заданных α, β с умножением множества, тип α ≃* β конечен.

LaTeX

$$$Fintype (\\alpha \\simeq^* \\beta)$$$

Lean4

@[to_additive]
instance instFintype {α β : Type*} [Mul α] [Mul β] [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
    Fintype (α ≃* β)
    where
  elems :=
    Equiv.instFintype.elems.filterMap
      (fun e => if h : ∀ a b : α, e (a * b) = e a * e b then (⟨e, h⟩ : α ≃* β) else none) (by aesop)
  complete
    me :=
    (Finset.mem_filterMap ..).mpr
      ⟨me.toEquiv, Finset.mem_univ _, by { simp; rfl
      }⟩

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