diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 55 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 38 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 15 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 15 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 5 |
9 files changed, 91 insertions, 63 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 2f5e844..1da8313 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -714,7 +714,7 @@ rewrite mul1n; apply/dvdn_biggcdP/(all_nthP 0)=> a_dv_p i ltip /=. exact: a_dv_p. Qed. -Lemma map_poly_divzK a p : +Lemma map_poly_divzK {a} p : p \is a polyOver (dvdz a) -> a *: map_poly (divz^~ a) p = p. Proof. move/polyOverP=> a_dv_p; apply/polyP=> i. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 3fe8d01..3b12802 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -916,9 +916,10 @@ Arguments row_mxA {R m n1 n2 n3 A1 A2 A3}. Arguments col_mxA {R m1 m2 m3 n A1 A2 A3}. Arguments block_mxA {R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33}. -Prenex Implicits castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx. +Prenex Implicits castmx trmx trmxK lsubmx rsubmx usubmx dsubmx row_mx col_mx. Prenex Implicits block_mx ulsubmx ursubmx dlsubmx drsubmx. Prenex Implicits mxvec vec_mx mxvec_indexP mxvecK vec_mxK. +Arguments trmx_inj {R m n} [A1 A2] eqA12t : rename. Notation "A ^T" := (trmx A) : ring_scope. @@ -1031,6 +1032,8 @@ End Block. End MapMatrix. +Arguments map_mx {aT rT} f {m n} A. + (*****************************************************************************) (********************* Matrix Zmodule (additive) structure *******************) (*****************************************************************************) @@ -1180,9 +1183,7 @@ Qed. Lemma col_mx_eq0 (m1 m2 n : nat) (A1 : 'M_(m1, n)) (A2 : 'M_(m2, n)): (col_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0). -Proof. -by rewrite -) !trmx0 tr_col_mx row_mx_eq0. -Qed. +Proof. by rewrite - !trmx0 tr_col_mx row_mx_eq0. Qed. Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : (block_mx Aul Aur Adl Adr == 0) = @@ -1332,29 +1333,29 @@ Proof. by rewrite {1}[u]matrix_sum_delta big_ord1. Qed. Lemma delta_mx_lshift m n1 n2 i j : delta_mx i (lshift n2 j) = row_mx (delta_mx i j) 0 :> 'M_(m, n1 + n2). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inl _ _)); case: split => ?; rewrite mxE ?andbF. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inl _ _)). +by case: split => ?; rewrite mxE ?andbF. Qed. Lemma delta_mx_rshift m n1 n2 i j : delta_mx i (rshift n1 j) = row_mx 0 (delta_mx i j) :> 'M_(m, n1 + n2). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inr _ _)); case: split => ?; rewrite mxE ?andbF. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inr _ _)). +by case: split => ?; rewrite mxE ?andbF. Qed. Lemma delta_mx_ushift m1 m2 n i j : delta_mx (lshift m2 i) j = col_mx (delta_mx i j) 0 :> 'M_(m1 + m2, n). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inl _ _)); case: split => ?; rewrite mxE. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inl _ _)). +by case: split => ?; rewrite mxE. Qed. Lemma delta_mx_dshift m1 m2 n i j : delta_mx (rshift m1 i) j = col_mx 0 (delta_mx i j) :> 'M_(m1 + m2, n). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inr _ _)); case: split => ?; rewrite mxE. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inr _ _)). +by case: split => ?; rewrite mxE. Qed. Lemma vec_mx_delta m n i j : @@ -1628,7 +1629,7 @@ Qed. Lemma mul_col_perm m n p s (A : 'M_(m, n)) (B : 'M_(n, p)) : col_perm s A *m B = A *m row_perm s^-1 B. Proof. -apply/matrixP=> i k; rewrite !mxE (reindex_inj (@perm_inj _ s^-1)). +apply/matrixP=> i k; rewrite !mxE (reindex_perm s^-1). by apply: eq_bigr => j _ /=; rewrite !mxE permKV. Qed. @@ -2013,7 +2014,7 @@ Lemma lift0_mx_perm s : lift0_mx (perm_mx s) = perm_mx (lift0_perm s). Proof. apply/matrixP=> /= i j; rewrite !mxE split1 /=; case: unliftP => [i'|] -> /=. rewrite lift0_perm_lift !mxE split1 /=. - by case: unliftP => [j'|] ->; rewrite ?(inj_eq (@lift_inj _ _)) /= !mxE. + by case: unliftP => [j'|] ->; rewrite ?(inj_eq (lift_inj _)) /= !mxE. rewrite lift0_perm0 !mxE split1 /=. by case: unliftP => [j'|] ->; rewrite /= mxE. Qed. @@ -2142,7 +2143,7 @@ Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n. Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed. Lemma map_mx_is_multiplicative n' (n := n'.+1) : - multiplicative ((map_mx f) n n). + multiplicative (map_mx f : 'M_n -> 'M_n). Proof. by split; [apply: map_mxM | apply: map_mx1]. Qed. Canonical map_mx_rmorphism n' := AddRMorphism (map_mx_is_multiplicative n'). @@ -2291,14 +2292,14 @@ rewrite [\det A](bigID (@odd_perm _)) /=. apply: canLR (subrK _) _; rewrite add0r -sumrN. rewrite (reindex_inj (mulgI t)); apply: eq_big => //= s. rewrite oddMt => /negPf->; rewrite mulN1r mul1r; congr (- _). -rewrite (reindex_inj (@perm_inj _ t)); apply: eq_bigr => /= i _. +rewrite (reindex_perm t); apply: eq_bigr => /= i _. by rewrite permM tpermK /t; case: tpermP => // ->; rewrite eqA12. Qed. Lemma det_tr n (A : 'M[R]_n) : \det A^T = \det A. Proof. -rewrite [\det A^T](reindex_inj (@invg_inj _)) /=. -apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_inj (@perm_inj _ s)) /=. +rewrite [\det A^T](reindex_inj invg_inj) /=. +apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_perm s) /=. by congr (_ * _); apply: eq_bigr => i _; rewrite mxE permK. Qed. @@ -2349,7 +2350,7 @@ rewrite (bigID (fun f : F => injectiveb f)) /= addrC big1 ?add0r => [|f Uf]. rewrite (reindex_inj (mulgI s)); apply: eq_bigr => t _ /=. rewrite big_split /= mulrA mulrCA mulrA mulrCA mulrA. rewrite -signr_addb odd_permM !pvalE; congr (_ * _); symmetry. - by rewrite (reindex_inj (@perm_inj _ s)); apply: eq_bigr => i; rewrite permM. + by rewrite (reindex_perm s); apply: eq_bigr => i; rewrite permM. transitivity (\det (\matrix_(i, j) B (f i) j) * \prod_i A i (f i)). rewrite mulrC big_distrr /=; apply: eq_bigr => s _. rewrite mulrCA big_split //=; congr (_ * (_ * _)). @@ -2382,7 +2383,7 @@ rewrite (reindex (lift_perm i0 j0)); last first. pose ulsf i (s : 'S_n.+1) k := odflt k (unlift (s i) (s (lift i k))). have ulsfK i (s : 'S_n.+1) k: lift (s i) (ulsf i s k) = s (lift i k). rewrite /ulsf; have:= neq_lift i k. - by rewrite -(inj_eq (@perm_inj _ s)) => /unlift_some[] ? ? ->. + by rewrite -(can_eq (permK s)) => /unlift_some[] ? ? ->. have inj_ulsf: injective (ulsf i0 _). move=> s; apply: can_inj (ulsf (s i0) s^-1%g) _ => k'. by rewrite {1}/ulsf ulsfK !permK liftK. @@ -2497,8 +2498,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed. End ComMatrix. -Arguments lin_mul_row {R m n}. -Arguments lin_mulmx {R m n p}. +Arguments lin_mul_row {R m n} u. +Arguments lin_mulmx {R m n p} A. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. @@ -2642,7 +2643,7 @@ Qed. End MatrixInv. -Prenex Implicits unitmx invmx. +Prenex Implicits unitmx invmx invmxK. Canonical matrix_countUnitRingType (R : countComUnitRingType) n := [countUnitRingType of 'M[R]_n.+1]. @@ -2790,7 +2791,7 @@ Section MapFieldMatrix. Variables (aF : fieldType) (rF : comUnitRingType) (f : {rmorphism aF -> rF}). Local Notation "A ^f" := (map_mx f A) : ring_scope. -Lemma map_mx_inj m n : injective ((map_mx f) m n). +Lemma map_mx_inj {m n} : injective (map_mx f : 'M_(m, n) -> 'M_(m, n)). Proof. move=> A B eq_AB; apply/matrixP=> i j. by move/matrixP/(_ i j): eq_AB; rewrite !mxE; apply: fmorph_inj. @@ -2811,7 +2812,7 @@ Proof. exact: map_unitmx. Qed. Lemma map_invmx n (A : 'M_n) : (invmx A)^f = invmx A^f. Proof. -rewrite /invmx map_unitmx (fun_if ((map_mx f) n n)). +rewrite /invmx map_unitmx (fun_if (map_mx f)). by rewrite map_mxZ map_mx_adj det_map_mx fmorphV. Qed. @@ -2819,10 +2820,12 @@ Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1. Proof. exact: map_invmx. Qed. Lemma map_mx_eq0 m n (A : 'M_(m, n)) : (A^f == 0) = (A == 0). -Proof. by rewrite -(inj_eq (@map_mx_inj m n)) raddf0. Qed. +Proof. by rewrite -(inj_eq map_mx_inj) raddf0. Qed. End MapFieldMatrix. +Arguments map_mx_inj {aF rF f m n} [A1 A2] eqA12f : rename. + (*****************************************************************************) (****************************** LUP decomposion ******************************) (*****************************************************************************) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index f679828..710adc6 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -29,7 +29,7 @@ Require Import poly polydiv. (* char_poly A == the characteristic polynomial of A. *) (* char_poly_mx A == a matrix whose determinant is char_poly A. *) (* companionmx p == a matrix whose char_poly is p *) -(* mxminpoly A == the minimal polynomial of A, i.e., the smallest monic *) +(* mxminpoly A == the minimal polynomial of A, i.e., the smallest monic *) (* polynomial that annihilates A (A must be nontrivial). *) (* degree_mxminpoly A == the (positive) degree of mxminpoly A. *) (* mx_inv_horner A == the inverse of horner_mx A for polynomials of degree *) @@ -116,8 +116,9 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear. End RowPoly. +Prenex Implicits rVpoly rVpolyK. Arguments poly_rV {R d}. -Prenex Implicits rVpoly. +Arguments poly_rV_K {R d} [p] le_p_d. Section Resultant. @@ -140,6 +141,8 @@ Definition resultant := \det Sylvester_mx. End Resultant. +Prenex Implicits Sylvester_mx resultant. + Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) : size p > 1 -> size q > 1 -> {uv : {poly R} * {poly R} | size uv.1 < size q /\ size uv.2 < size p @@ -224,7 +227,7 @@ apply/det0P/idP=> [[uv nz_uv] | r_nonC]. rewrite addrC addr_eq0 => /eqP vq_up. have nz_v: v != 0. apply: contraNneq nz_uv => v0; apply/eqP. - congr row_mx; apply: (can_inj (@rVpolyK _ _)); rewrite linear0 // -/u. + congr row_mx; apply: (can_inj rVpolyK); rewrite linear0 // -/u. by apply: contra_eq vq_up; rewrite v0 mul0r -addr_eq0 add0r => /mulf_neq0->. have r_nz: r != 0 := dvdpN0 r_p p_nz. have /dvdpP [[c w] /= nz_c wv]: v %| m by rewrite dvdp_gcd !dvdp_mulr. @@ -298,6 +301,8 @@ Qed. End HornerMx. +Prenex Implicits horner_mx powers_mx. + Section CharPoly. Variables (R : ringType) (n : nat) (A : 'M[R]_n). @@ -330,7 +335,7 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1). by rewrite sub0r size_opp size_polyC leq_b1. rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS. apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j. -rewrite !inE -{1}fix_j (inj_eq (@perm_inj _ s)) orbb. +rewrite !inE -{1}fix_j (inj_eq perm_inj) orbb. by apply: contraNneq nfix_i => <-; rewrite fix_j. Qed. @@ -373,6 +378,8 @@ Qed. End CharPoly. +Prenex Implicits char_poly_mx char_poly. + Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) : exists phi : {rmorphism 'M[{poly R}]_n -> {poly 'M[R]_n}}, [/\ bijective phi, @@ -431,13 +438,11 @@ rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)). by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn). Qed. -Section Companion. - -Definition companionmx (R : ringType) (p : seq R) (d := (size p).-1) := +Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) := \matrix_(i < d, j < d) if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R. -Lemma companionmxK (R : comRingType) (p : {poly R}) : +Lemma companionmxK {R : comRingType} (p : {poly R}) : p \is monic -> char_poly (companionmx p) = p. Proof. pose D n : 'M[{poly R}]_n := \matrix_(i, j) @@ -487,8 +492,6 @@ rewrite ltn_eqF ?big1 ?addr0 1?eq_sym //; last first. by move=> k /negPf ki_eqF; rewrite !mxE eqxx ki_eqF mul0r. Qed. -End Companion. - Section MinPoly. Variables (F : fieldType) (n' : nat). @@ -601,10 +604,10 @@ Qed. Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p. Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed. -Lemma horner_rVpoly_inj : @injective 'M_n 'rV_d (horner_mx A \o rVpoly). +Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n). Proof. -apply: can_inj (poly_rV \o mx_inv_horner) _ => u. -by rewrite /= horner_rVpolyK rVpolyK. +apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=. +by rewrite horner_rVpolyK rVpolyK. Qed. Lemma mxminpoly_linear_is_scalar : (d <= 1) = is_scalar_mx A. @@ -639,6 +642,11 @@ Qed. End MinPoly. +Prenex Implicits degree_mxminpoly mxminpoly mx_inv_horner. + +Arguments mx_inv_hornerK {F n' A} [B] AnB. +Arguments horner_rVpoly_inj {F n' A} [u1 u2] eq_u12A : rename. + (* Parametricity. *) Section MapRingMatrix. @@ -1044,9 +1052,9 @@ Local Notation holds := GRing.holds. Local Notation qf_form := GRing.qf_form. Local Notation qf_eval := GRing.qf_eval. -Definition eval_mx (e : seq F) := map_mx (eval e). +Definition eval_mx (e : seq F) := @map_mx term F (eval e). -Definition mx_term := map_mx (@GRing.Const F). +Definition mx_term := @map_mx F term GRing.Const. Lemma eval_mx_term e m n (A : 'M_(m, n)) : eval_mx e (mx_term A) = A. Proof. by apply/matrixP=> i j; rewrite !mxE. Qed. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 929c313..702dfc4 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -142,8 +142,8 @@ Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i. End Polynomial. -(* We need to break off the section here to let the argument scope *) -(* directives take effect. *) +(* We need to break off the section here to let the Bind Scope directives *) +(* take effect. *) Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. Arguments polyseq {R} p%R. @@ -1675,7 +1675,7 @@ Qed. End PolynomialTheory. -Prenex Implicits polyC Poly lead_coef root horner polyOver. +Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver. Arguments monic {R}. Notation "\poly_ ( i < n ) E" := (poly n (fun i => E)) : ring_scope. Notation "c %:P" := (polyC c) : ring_scope. @@ -1694,6 +1694,7 @@ Arguments rootPf {R p x}. Arguments rootPt {R p x}. Arguments unity_rootP {R n z}. Arguments polyOverP {R S0 addS kS p}. +Arguments polyC_inj {R} [x1 x2] eq_x12P. Canonical polynomial_countZmodType (R : countRingType) := [countZmodType of polynomial R]. @@ -1947,7 +1948,7 @@ Definition comp_poly q p := p^:P.[q]. Local Notation "p \Po q" := (comp_poly q p) : ring_scope. Lemma size_map_polyC p : size p^:P = size p. -Proof. exact: size_map_inj_poly (@polyC_inj R) _ _. Qed. +Proof. exact/(size_map_inj_poly polyC_inj). Qed. Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0). Proof. by rewrite -!size_poly_eq0 size_map_polyC. Qed. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 40a1f83..47cee1f 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -875,6 +875,7 @@ End ZmoduleTheory. Arguments addrI {V} y [x1 x2]. Arguments addIr {V} x [x1 x2]. +Arguments opprK {V}. Arguments oppr_inj {V} [x1 x2]. Module Ring. @@ -3031,6 +3032,7 @@ End ClosedPredicates. End UnitRingTheory. +Arguments invrK {R}. Arguments invr_inj {R} [x1 x2]. Section UnitRingMorphism. @@ -5370,7 +5372,8 @@ Arguments addrI {V} y [x1 x2]. Arguments addIr {V} x [x1 x2]. Arguments subrI {V} y [x1 x2]. Arguments subIr {V} x [x1 x2]. -Definition opprK := opprK. +Definition opprK := @opprK. +Arguments opprK {V}. Definition oppr_inj := @oppr_inj. Arguments oppr_inj {V} [x1 x2]. Definition oppr0 := oppr0. @@ -5554,7 +5557,8 @@ Definition divIr := divIr. Definition telescope_prodr := telescope_prodr. Definition commrV := commrV. Definition unitrE := unitrE. -Definition invrK := invrK. +Definition invrK := @invrK. +Arguments invrK {R}. Definition invr_inj := @invr_inj. Arguments invr_inj {R} [x1 x2]. Definition unitrV := unitrV. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index b734ad7..e6b0264 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -290,7 +290,7 @@ Lemma mulz_addl : left_distributive mulz (+%R). Proof. move=> x y z; elim: z=> [|n|n]; first by rewrite !(mul0z,mulzC). by rewrite !mulzS=> ->; rewrite !addrA [X in X + _]addrAC. -rewrite !mulzN !mulzS -!opprD=> /(inv_inj (@opprK _))->. +rewrite !mulzN !mulzS -!opprD=> /oppr_inj->. by rewrite !addrA [X in X + _]addrAC. Qed. @@ -330,22 +330,21 @@ Lemma mulVz : {in unitz, left_inverse 1%R invz *%R}. Proof. by move=> n /pred2P[] ->. Qed. Lemma mulzn_eq1 m (n : nat) : (m * n == 1) = (m == 1) && (n == 1%N). -Proof. by case: m=> m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed. +Proof. by case: m => m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed. Lemma unitzPl m n : n * m = 1 -> m \is a unitz. Proof. -case: m => m; move/eqP; rewrite qualifE. -* by rewrite mulzn_eq1; case/andP=> _; move/eqP->. -* by rewrite NegzE intS mulrN -mulNr mulzn_eq1; case/andP=> _. +rewrite qualifE => /eqP. +by case: m => m; rewrite ?NegzE ?mulrN -?mulNr mulzn_eq1 => /andP[_ /eqP->]. Qed. -Lemma invz_out : {in [predC unitz], invz =1 id}. +Lemma invz_out : {in [predC unitz], invz =1 id}. Proof. exact. Qed. Lemma idomain_axiomz m n : m * n = 0 -> (m == 0) || (n == 0). Proof. -by case: m n => m [] n //=; move/eqP; rewrite ?(NegzE,mulrN,mulNr); - rewrite ?(inv_eq (@opprK _)) -PoszM [_==_]muln_eq0. +by case: m n => m [] n //= /eqP; + rewrite ?(NegzE, mulrN, mulNr) ?oppr_eq0 -PoszM [_ == _]muln_eq0. Qed. Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2414e13..ec932a1 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1457,18 +1457,18 @@ Hint Resolve ltr_opp2 : core. Definition lter_opp2 := (ler_opp2, ltr_opp2). Lemma ler_oppr x y : (x <= - y) = (y <= - x). -Proof. by rewrite (monoRL (@opprK _) ler_opp2). Qed. +Proof. by rewrite (monoRL opprK ler_opp2). Qed. Lemma ltr_oppr x y : (x < - y) = (y < - x). -Proof. by rewrite (monoRL (@opprK _) (lerW_nmono _)). Qed. +Proof. by rewrite (monoRL opprK (lerW_nmono _)). Qed. Definition lter_oppr := (ler_oppr, ltr_oppr). Lemma ler_oppl x y : (- x <= y) = (- y <= x). -Proof. by rewrite (monoLR (@opprK _) ler_opp2). Qed. +Proof. by rewrite (monoLR opprK ler_opp2). Qed. Lemma ltr_oppl x y : (- x < y) = (- y < x). -Proof. by rewrite (monoLR (@opprK _) (lerW_nmono _)). Qed. +Proof. by rewrite (monoLR opprK (lerW_nmono _)). Qed. Definition lter_oppl := (ler_oppl, ltr_oppl). @@ -4797,12 +4797,17 @@ Qed. End ClosedFieldTheory. -Notation "n .-root" := (@nthroot _ n) (at level 2, format "n .-root") : ring_scope. +Notation "n .-root" := (@nthroot _ n) + (at level 2, format "n .-root") : ring_scope. Notation sqrtC := 2.-root. Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope. Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope. Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope. +Arguments conjCK {C} x. +Arguments sqrCK {C} [x] le0x. +Arguments sqrCK_P {C x}. + End Theory. Module RealMixin. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index c4c62c3..4766c74 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1355,6 +1355,8 @@ Proof. by elim/big_rec2: _ => [|i _ f _ <-]; rewrite lfunE. Qed. End LfunZmodType. +Arguments fun_of_lfunK {R aT rT}. + Section LfunVectType. Variables (R : comRingType) (aT rT : vectType R). @@ -1603,6 +1605,7 @@ Arguments lfunPn {K aT rT f g}. Arguments lker0P {K aT rT f}. Arguments eqlfunP {K aT rT f g v}. Arguments eqlfun_inP {K aT rT V f g}. +Arguments limg_lfunVK {K aT rT f} [x] f_x. Section FixedSpace. @@ -1718,6 +1721,8 @@ Qed. End LinearPreimage. +Arguments lpreimK {K aT rT f} [W] fW. + Section LfunAlgebra. (* This section is a bit of a place holder: the instances we build here can't *) (* be canonical because we are missing an interface for proper vectTypes, *) @@ -1944,7 +1949,7 @@ Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin. End SubVector. Prenex Implicits vsval vsproj vsvalK. Arguments subvs_inj {K vT U} [x1 x2]. -Arguments vsprojK {K vT U} [x]. +Arguments vsprojK {K vT U} [x] Ux. Section MatrixVectType. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index ba6c1b3..5e931ef 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -180,7 +180,8 @@ End ZpDef. Arguments Zp0 {p'}. Arguments Zp1 {p'}. -Arguments inZp {p'}. +Arguments inZp {p'} i. +Arguments valZpK {p'} x. Lemma ord1 : all_equal_to (0 : 'I_1). Proof. by case=> [[] // ?]; apply: val_inj. Qed. @@ -259,6 +260,8 @@ Notation "''Z_' p" := 'I_(Zp_trunc p).+2 Notation "''F_' p" := 'Z_(pdiv p) (at level 8, p at level 2, format "''F_' p") : type_scope. +Arguments natr_Zp {p'} x. + Section Groups. Variable p : nat. |