From db04fdb3b4a7e1ee401ee6a6a8d787c1af72fdc0 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 26 Aug 2025 16:52:09 +0200 Subject: [PATCH 1/2] Generalize expcmn to expmn, which works for any monomType --- src/monalg.v | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/src/monalg.v b/src/monalg.v index 9ac128d..716b9dc 100644 --- a/src/monalg.v +++ b/src/monalg.v @@ -137,11 +137,27 @@ Local Open Scope monom_scope. #[export] HB.instance Definition _ := Monoid.isLaw.Build M 1 mmul mulmA mul1m mulm1. +Definition expmn (x : M) (n : nat) : M := iterop n *%M x 1%M. + +Arguments expmn : simpl never. + Lemma unitmP (x y : M) : reflect (x == 1 /\ y == 1) (x * y == 1). Proof. by apply: (iffP eqP)=> [/unitm[-> ->]|[/eqP-> /eqP->]] //; rewrite mulm1. Qed. +Lemma expmnS (x : M) (n : nat) : expmn x n.+1 = x * expmn x n. +Proof. by rewrite /expmn !Monoid.iteropE iterS. Qed. + +Lemma expmnD (x : M) (n m : nat) : expmn x (n + m) = expmn x n * expmn x m. +Proof. +elim: n => [|n IHn]; first by rewrite mul1m. +by rewrite addSn !expmnS IHn mulmA. +Qed. + +Lemma expmnSr (x : M) (n : nat) : expmn x n.+1 = expmn x n * x. +Proof. by rewrite -addn1 expmnD. Qed. + End Monomial. #[export] @@ -1414,8 +1430,6 @@ Definition mulcm m1 m2 : cmonom I := Definition divcm m1 m2 : cmonom I := [cmonom m1 i - m2 i | i in finsupp m1]%M. -Definition expcmn m n : cmonom I := iterop n mulcm m onecm. - Lemma onecmE i : onecm i = 0%N. Proof. by rewrite fsfun_ffun insubF. Qed. @@ -1454,6 +1468,9 @@ HB.instance Definition _ := Choice_isMonomialDef.Build (cmonom I) mulcmA mul0cm mulcm0 mulcm_eq0. HB.instance Definition _ := MonomialDef_isConomialDef.Build (cmonom I) mulcmC. +#[deprecated(since="multinomials 2.5.0", use=expmn)] +Definition expcmn m n : cmonom I := expmn m n. + End CmonomCanonicals. (* -------------------------------------------------------------------- *) From 78d1a3bf22bdd0154b0b26011330ba100bc5cf4e Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 27 Aug 2025 16:47:33 +0200 Subject: [PATCH 2/2] Generalize cmM_eq1 and fmM_eq1 to mulm_eq1 --- src/monalg.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/monalg.v b/src/monalg.v index 716b9dc..3e07e49 100644 --- a/src/monalg.v +++ b/src/monalg.v @@ -146,6 +146,9 @@ Proof. by apply: (iffP eqP)=> [/unitm[-> ->]|[/eqP-> /eqP->]] //; rewrite mulm1. Qed. +Lemma mulm_eq1 (x y : M) : (x * y == 1) = (x == 1) && (y == 1). +Proof. exact/unitmP/andP. Qed. + Lemma expmnS (x : M) (n : nat) : expmn x n.+1 = x * expmn x n. Proof. by rewrite /expmn !Monoid.iteropE iterS. Qed. @@ -1569,8 +1572,9 @@ Qed. Lemma mdeg_eq0 m : (mdeg m == 0%N) = (m == 1%M). Proof. exact/mf_eq0. Qed. +#[deprecated(since="multinomials 2.5.0", use=mulm_eq1)] Lemma cmM_eq1 m1 m2 : (m1 * m2 == 1)%M = (m1 == 1%M) && (m2 == 1%M). -Proof. by rewrite -!mdeg_eq0 mdegM addn_eq0. Qed. +Proof. exact: mulm_eq1. Qed. Lemma cm1_eq1 i : (U_(i) == 1)%M = false. Proof. by rewrite -mdeg_eq0 mdegU. Qed. @@ -1778,8 +1782,9 @@ Qed. Lemma fdeg_eq0 m : (fdeg m == 0%N) = (m == 1%M). Proof. exact/mf_eq0. Qed. +#[deprecated(since="multinomials 2.5.0", use=mulm_eq1)] Lemma fmM_eq1 m1 m2 : (m1 * m2 == 1)%M = (m1 == 1%M) && (m2 == 1%M). -Proof. by rewrite -!fdeg_eq0 fdegM addn_eq0. Qed. +Proof. exact: mulm_eq1. Qed. Lemma fm1_eq1 i : (U_(i) == 1)%M = false. Proof. by rewrite -fdeg_eq0 fdegU. Qed.