Divisibility in finite types

instance instDecidableDvdOfFintypeOfDecidableEq {M : Type u_1} [Semigroup M] [Fintype M] [DecidableEq M] (a b : M) : Decidable (a ∣ b)

Equations

• instDecidableDvdOfFintypeOfDecidableEq a b = decidable_of_iff (∃ (c : M), b = a * c) ⋯