diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algnum.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index fcd6c2d..5d78cac 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -354,10 +354,10 @@ Lemma extend_algC_subfield_aut (Qs : fieldExtType rat) Proof. pose numF_inj (Qr : fieldExtType rat) := {rmorphism Qr -> algC}. pose subAut := {Qr : _ & numF_inj Qr * {lrmorphism Qr -> Qr}}%type. -pose SubAut := existS _ _ (_, _) : subAut. -pose Sdom (mu : subAut) := projS1 mu. -pose Sinj (mu : subAut) : {rmorphism Sdom mu -> algC} := (projS2 mu).1. -pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projS2 mu).2. +pose SubAut := existT _ _ (_, _) : subAut. +pose Sdom (mu : subAut) := projT1 mu. +pose Sinj (mu : subAut) : {rmorphism Sdom mu -> algC} := (projT2 mu).1. +pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projT2 mu).2. have SinjZ Qr (QrC : numF_inj Qr) a x: QrC (a *: x) = QtoC a * QrC x. rewrite mulrAC; apply: canRL (mulfK _) _. by rewrite intr_eq0 denq_neq0. |