From c6e0d703165b0c60c270672eb542aa8934929bfe Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 9 Oct 2020 00:21:00 +0900 Subject: Switch from long suffixes to short suffixes --- mathcomp/field/falgebra.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/field/falgebra.v') diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index bdff38a..db235fe 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1173,11 +1173,11 @@ by rewrite -aimgM limgS // [rhs in (_ <= rhs)%VS]agenvEl addvSr. Qed. Lemma aimg_adjoin (f : ahom aT rT) U x : (f @: <> = <>)%VS. -Proof. by rewrite aimg_agen limg_add limg_line. Qed. +Proof. by rewrite aimg_agen limgD limg_line. Qed. Lemma aimg_adjoin_seq (f : ahom aT rT) U xs : (f @: <> = <>)%VS. -Proof. by rewrite aimg_agen limg_add limg_span. Qed. +Proof. by rewrite aimg_agen limgD limg_span. Qed. Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) : is_aspace (lker (ahval f - ahval g)). -- cgit v1.2.3