type problem

Stream: new members

[vxctyxeha]

import Mathlib

open Fintype Set Real Ideal Polynomial

open scoped BigOperators

theorem my_favorite_theorem : ¬ CommGroup (DihedralGroup 4) :=

sorry

[vxctyxeha]

pplication type mismatch: The argument
CommGroup (DihedralGroup 4)
has type
Type
of sort Type 1 but is expected to have type
Prop
of sort Type in the application
¬CommGroup (DihedralGroup 4)

[Niels Voss]

CommGroup X is a type, not a proposition. You normally would like to show IsEmpty (CommGroup (DihedralGroup 4)). But this is actually wrong as well, but for a different reason: DihedralGroup already has a group instance on it, but your statement says that there are no commutative groups on DihedralGroup at all, which is false. Instead, you probably want to show ¬ IsMulCommutative (DihedralGroup 4).

[vxctyxeha]

import Mathlib

open DihedralGroup

theorem my_favorite_theorem : ¬ IsMulCommutative (DihedralGroup 4) := by
  -- Show that multiplication is not commutative by providing a counterexample
  sorry

function expected at
IsMulCommutative
term has type
?m.3

[Robin Arnez]

You're probably on an older version of mathlib. Try Std.Commutative (α := DihedralGroup 4) (· * ·)