diff options
| author | Cyril Cohen | 2020-10-30 18:50:56 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:50:56 +0100 |
| commit | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/field/falgebra.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
| parent | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (diff) | |
Merge pull request #607 from pi8027/distr-suffixes
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/field/falgebra.v')
| -rw-r--r-- | mathcomp/field/falgebra.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 @: <<U; x>> = <<f @: U; f x>>)%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 @: <<U & xs>> = <<f @: U & map f xs>>)%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)). |