]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/algebra/finite_groups.ma
A very nice experiment using notation: we define the notation for natural
[helm.git] / helm / software / matita / library / algebra / finite_groups.ma
index 8b1beb7027e18648a6948f178931bcf64915d6da..d3f5cf27294cba1f71251cf9b9b5f46edffd8277 100644 (file)
@@ -46,7 +46,7 @@ interpretation "Finite_enumerable representation" 'repr S i =
  (cic:/matita/algebra/finite_groups/repr.con S
   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
 
-notation "hvbox(ι e)" with precedence 60
+notation "hvbox(\iota e)" with precedence 60
 for @{ 'index_of_finite_enumerable_semigroup $e }.
 
 interpretation "Index_of_finite_enumerable representation"