From f6d22c0002fbebc554de08e56b95b61455296982 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 11 Oct 2015 12:22:12 -0700 Subject: [PATCH] fix(library/theories/group_theory/finsubg): fix compilation errors --- library/theories/group_theory/finsubg.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean index 7074531ff..67dff7079 100644 --- a/library/theories/group_theory/finsubg.lean +++ b/library/theories/group_theory/finsubg.lean @@ -84,7 +84,7 @@ definition fin_rcoset (H : finset A) (a : A) : finset A := image (rmul_by a) H definition fin_lcosets (H G : finset A) := image (fin_lcoset H) G -definition fin_inv : finset A → finset A := image has_inv.inv +definition fin_inv : finset A → finset A := image inv variable {H : finset A}