From 9dd5ca125071c4e57e864db6aff54dbac2b34d0a Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 9 Oct 2024 18:04:41 +0200 Subject: [PATCH] annotate card_vspace1 --- theories/BGappendixC.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v index dd4bf95..e6b3085 100644 --- a/theories/BGappendixC.v +++ b/theories/BGappendixC.v @@ -55,7 +55,10 @@ Let Fp : {vspace F} := 1%VS. Hypothesis oF : #|F| = (p ^ q)%N. Let oF_p : #|'F_p| = p. Proof. exact: card_Fp. Qed. -Let oFp : #|Fp| = p. Proof. by rewrite card_vspace1. Qed. +Let oFp : #|Fp| = p. +Proof. +by rewrite (@card_vspace1 _ _ (Falgebra.class (PrimeCharType _))). +Qed. Let oFpq : #|Fpq| = (p ^ q)%N. Proof. by rewrite card_vspacef. Qed. Let dimFpq : \dim Fpq = q. Proof. by rewrite primeChar_dimf oF pfactorK. Qed.