decidableEqMulEquivFintype — Mathlib

English

There exists a decidable equality on the set of multiplicative equivalences between α and β, provided α is finite and β has a decidable equality.

Русский

Существует разрешимая равенство на множестве мультипликативных эквивалентностей между α и β, если α конечно и β имеет разрешимое равенство.

LaTeX

$$$\operatorname{DecidableEq}(\alpha \simeq^* \beta)$$$

Lean4

@[to_additive]
instance decidableEqMulEquivFintype {α β : Type*} [DecidableEq β] [Fintype α] [Mul α] [Mul β] : DecidableEq (α ≃* β) :=
  fun a b => decidable_of_iff ((a : α → β) = b) (Injective.eq_iff DFunLike.coe_injective)

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