-
Definition char (
R :
Ring.type)
of phant R :
nat_pred :=
-
[pred p | prime p & p%:R == 0
:> R].
+
Definition char (
R :
Ring.type)
of phant R :
nat_pred :=
+
[pred p | prime p & p%:R == 0
:> R].
@@ -1077,22 +1090,22 @@
Implicit Types x y :
R.
-
Lemma mulrA : @
associative R *%R.
-
Lemma mul1r : @
left_id R R 1
*%R.
-
Lemma mulr1 : @
right_id R R 1
*%R.
-
Lemma mulrDl : @
left_distributive R R *%R +%R.
-
Lemma mulrDr : @
right_distributive R R *%R +%R.
-
Lemma oner_neq0 : 1
!= 0
:> R.
-
Lemma oner_eq0 :
(1
== 0
:> R) = false.
+
Lemma mulrA : @
associative R *%R.
+
Lemma mul1r : @
left_id R R 1
*%R.
+
Lemma mulr1 : @
right_id R R 1
*%R.
+
Lemma mulrDl : @
left_distributive R R *%R +%R.
+
Lemma mulrDr : @
right_distributive R R *%R +%R.
+
Lemma oner_neq0 : 1
!= 0
:> R.
+
Lemma oner_eq0 :
(1
== 0
:> R) = false.
-
Lemma mul0r : @
left_zero R R 0
*%R.
-
Lemma mulr0 : @
right_zero R R 0
*%R.
-
Lemma mulrN x y :
x × (- y) = - (x × y).
-
Lemma mulNr x y :
(- x) × y = - (x × y).
-
Lemma mulrNN x y :
(- x) × (- y) = x × y.
-
Lemma mulN1r x : -1
× x = - x.
-
Lemma mulrN1 x :
x × -1
= - x.
+
Lemma mul0r : @
left_zero R R 0
*%R.
+
Lemma mulr0 : @
right_zero R R 0
*%R.
+
Lemma mulrN x y :
x × (- y) = - (x × y).
+
Lemma mulNr x y :
(- x) × y = - (x × y).
+
Lemma mulrNN x y :
(- x) × (- y) = x × y.
+
Lemma mulN1r x : -1
× x = - x.
+
Lemma mulrN1 x :
x × -1
= - x.
Canonical mul_monoid :=
Monoid.Law mulrA mul1r mulr1.
@@ -1100,65 +1113,65 @@
Canonical addoid :=
Monoid.AddLaw mulrDl mulrDr.
-
Lemma mulr_suml I r P (
F :
I → R)
x :
-
(\sum_(i <- r | P i) F i) × x = \sum_(i <- r | P i) F i × x.
+
Lemma mulr_suml I r P (
F :
I → R)
x :
+
(\sum_(i <- r | P i) F i) × x = \sum_(i <- r | P i) F i × x.
-
Lemma mulr_sumr I r P (
F :
I → R)
x :
-
x × (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x × F i.
+
Lemma mulr_sumr I r P (
F :
I → R)
x :
+
x × (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x × F i.
-
Lemma mulrBl x y z :
(y - z) × x = y × x - z × x.
+
Lemma mulrBl x y z :
(y - z) × x = y × x - z × x.
-
Lemma mulrBr x y z :
x × (y - z) = x × y - x × z.
+
Lemma mulrBr x y z :
x × (y - z) = x × y - x × z.
-
Lemma mulrnAl x y n :
(x *+ n) × y = (x × y) *+ n.
+
Lemma mulrnAl x y n :
(x *+ n) × y = (x × y) *+ n.
-
Lemma mulrnAr x y n :
x × (y *+ n) = (x × y) *+ n.
+
Lemma mulrnAr x y n :
x × (y *+ n) = (x × y) *+ n.
-
Lemma mulr_natl x n :
n%:R × x = x *+ n.
+
Lemma mulr_natl x n :
n%:R × x = x *+ n.
-
Lemma mulr_natr x n :
x × n%:R = x *+ n.
+
Lemma mulr_natr x n :
x × n%:R = x *+ n.
-
Lemma natrD m n :
(m + n)%:R = m%:R + n%:R :> R.
+
Lemma natrD m n :
(m + n)%:R = m%:R + n%:R :> R.
-
Lemma natrB m n :
n ≤ m → (m - n)%:R = m%:R - n%:R :> R.
+
Lemma natrB m n :
n ≤ m → (m - n)%:R = m%:R - n%:R :> R.
Definition natr_sum :=
big_morph (
natmul 1)
natrD (
mulr0n 1).
-
Lemma natrM m n :
(m × n)%:R = m%:R × n%:R :> R.
+
Lemma natrM m n :
(m × n)%:R = m%:R × n%:R :> R.
-
Lemma expr0 x :
x ^+ 0
= 1.
-
Lemma expr1 x :
x ^+ 1
= x.
-
Lemma expr2 x :
x ^+ 2
= x × x.
+
Lemma expr0 x :
x ^+ 0
= 1.
+
Lemma expr1 x :
x ^+ 1
= x.
+
Lemma expr2 x :
x ^+ 2
= x × x.
-
Lemma exprS x n :
x ^+ n.+1 = x × x ^+ n.
+
Lemma exprS x n :
x ^+ n.+1 = x × x ^+ n.
-
Lemma expr0n n : 0
^+ n = (n == 0%
N)%:R :> R.
+
Lemma expr0n n : 0
^+ n = (n == 0%
N)%:R :> R.
-
Lemma expr1n n : 1
^+ n = 1
:> R.
+
Lemma expr1n n : 1
^+ n = 1
:> R.
-
Lemma exprD x m n :
x ^+ (m + n) = x ^+ m × x ^+ n.
+
Lemma exprD x m n :
x ^+ (m + n) = x ^+ m × x ^+ n.
-
Lemma exprSr x n :
x ^+ n.+1 = x ^+ n × x.
+
Lemma exprSr x n :
x ^+ n.+1 = x ^+ n × x.
-
Lemma commr_sym x y :
comm x y → comm y x.
+
Lemma commr_sym x y :
comm x y → comm y x.
Lemma commr_refl x :
comm x x.
@@ -1168,296 +1181,299 @@
Lemma commr1 x :
comm x 1.
-
Lemma commrN x y :
comm x y → comm x (
- y).
+
Lemma commrN x y :
comm x y → comm x (
- y).
Lemma commrN1 x :
comm x (-1).
-
Lemma commrD x y z :
comm x y → comm x z → comm x (
y + z).
+
Lemma commrD x y z :
comm x y → comm x z → comm x (
y + z).
-
Lemma commrMn x y n :
comm x y → comm x (
y *+ n).
+
Lemma commrMn x y n :
comm x y → comm x (
y *+ n).
-
Lemma commrM x y z :
comm x y → comm x z → comm x (
y × z).
+
Lemma commrM x y z :
comm x y → comm x z → comm x (
y × z).
-
Lemma commr_nat x n :
comm x n%:R.
+
Lemma commr_nat x n :
comm x n%:R.
-
Lemma commrX x y n :
comm x y → comm x (
y ^+ n).
+
Lemma commrX x y n :
comm x y → comm x (
y ^+ n).
-
Lemma exprMn_comm x y n :
comm x y → (x × y) ^+ n = x ^+ n × y ^+ n.
+
Lemma exprMn_comm x y n :
comm x y → (x × y) ^+ n = x ^+ n × y ^+ n.
-
Lemma commr_sign x n :
comm x (
(-1
) ^+ n).
+
Lemma commr_sign x n :
comm x (
(-1
) ^+ n).
-
Lemma exprMn_n x m n :
(x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.
+
Lemma exprMn_n x m n :
(x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.
-
Lemma exprM x m n :
x ^+ (m × n) = x ^+ m ^+ n.
+
Lemma exprM x m n :
x ^+ (m × n) = x ^+ m ^+ n.
-
Lemma exprAC x m n :
(x ^+ m) ^+ n = (x ^+ n) ^+ m.
+
Lemma exprAC x m n :
(x ^+ m) ^+ n = (x ^+ n) ^+ m.
-
Lemma expr_mod n x i :
x ^+ n = 1
→ x ^+ (i %% n) = x ^+ i.
+
Lemma expr_mod n x i :
x ^+ n = 1
→ x ^+ (i %% n) = x ^+ i.
-
Lemma expr_dvd n x i :
x ^+ n = 1
→ n %| i → x ^+ i = 1.
+
Lemma expr_dvd n x i :
x ^+ n = 1
→ n %| i → x ^+ i = 1.
-
Lemma natrX n k :
(n ^ k)%:R = n%:R ^+ k :> R.
+
Lemma natrX n k :
(n ^ k)%:R = n%:R ^+ k :> R.
-
Lemma signr_odd n :
(-1
) ^+ (odd n) = (-1
) ^+ n :> R.
+
Lemma signr_odd n :
(-1
) ^+ (odd n) = (-1
) ^+ n :> R.
-
Lemma signr_eq0 n :
((-1
) ^+ n == 0
:> R) = false.
+
Lemma signr_eq0 n :
((-1
) ^+ n == 0
:> R) = false.
-
Lemma mulr_sign (
b :
bool)
x :
(-1
) ^+ b × x = (if b then - x else x).
+
Lemma mulr_sign (
b :
bool)
x :
(-1
) ^+ b × x = (if b then - x else x).
-
Lemma signr_addb b1 b2 :
(-1
) ^+ (b1 (+) b2) = (-1
) ^+ b1 × (-1
) ^+ b2 :> R.
+
Lemma signr_addb b1 b2 :
(-1
) ^+ (b1 (+) b2) = (-1
) ^+ b1 × (-1
) ^+ b2 :> R.
-
Lemma signrE (
b :
bool) :
(-1
) ^+ b = 1
- b.*2%:R :> R.
+
Lemma signrE (
b :
bool) :
(-1
) ^+ b = 1
- b.*2%:R :> R.
-
Lemma signrN b :
(-1
) ^+ (~~ b) = - (-1
) ^+ b :> R.
+
Lemma signrN b :
(-1
) ^+ (~~ b) = - (-1
) ^+ b :> R.
-
Lemma mulr_signM (
b1 b2 :
bool)
x1 x2 :
-
((-1
) ^+ b1 × x1) × ((-1
) ^+ b2 × x2) = (-1
) ^+ (b1 (+) b2) × (x1 × x2).
+
Lemma mulr_signM (
b1 b2 :
bool)
x1 x2 :
+
((-1
) ^+ b1 × x1) × ((-1
) ^+ b2 × x2) = (-1
) ^+ (b1 (+) b2) × (x1 × x2).
-
Lemma exprNn x n :
(- x) ^+ n = (-1
) ^+ n × x ^+ n :> R.
+
Lemma exprNn x n :
(- x) ^+ n = (-1
) ^+ n × x ^+ n :> R.
-
Lemma sqrrN x :
(- x) ^+ 2
= x ^+ 2.
+
Lemma sqrrN x :
(- x) ^+ 2
= x ^+ 2.
-
Lemma sqrr_sign n :
((-1
) ^+ n) ^+ 2
= 1
:> R.
+
Lemma sqrr_sign n :
((-1
) ^+ n) ^+ 2
= 1
:> R.
-
Lemma signrMK n : @
involutive R (
*%R ((-1) ^+ n)).
+
Lemma signrMK n : @
involutive R (
*%R ((-1) ^+ n)).
-
Lemma mulrI_eq0 x y :
lreg x → (x × y == 0
) = (y == 0
).
+
Lemma lastr_eq0 (
s :
seq R)
x :
x != 0
→ (last x s == 0
) = (last 1
s == 0
).
-
Lemma lreg_neq0 x :
lreg x → x != 0.
+
Lemma mulrI_eq0 x y :
lreg x → (x × y == 0
) = (y == 0
).
-
Lemma mulrI0_lreg x :
(∀ y,
x × y = 0
→ y = 0
) → lreg x.
+
Lemma lreg_neq0 x :
lreg x → x != 0.
+
+
+
Lemma mulrI0_lreg x :
(∀ y,
x × y = 0
→ y = 0
) → lreg x.
-
Lemma lregN x :
lreg x → lreg (
- x).
+
Lemma lregN x :
lreg x → lreg (
- x).
-
Lemma lreg1 :
lreg (1
: R).
+
Lemma lreg1 :
lreg (1
: R).
-
Lemma lregM x y :
lreg x → lreg y → lreg (
x × y).
+
Lemma lregM x y :
lreg x → lreg y → lreg (
x × y).
-
Lemma lregX x n :
lreg x → lreg (
x ^+ n).
+
Lemma lregX x n :
lreg x → lreg (
x ^+ n).
-
Lemma lreg_sign n :
lreg (
(-1
) ^+ n : R).
+
Lemma lreg_sign n :
lreg (
(-1
) ^+ n : R).
-
Lemma prodr_const (
I :
finType) (
A :
pred I) (
x :
R) :
-
\prod_(i in A) x = x ^+ #|A|.
+
Lemma prodr_const (
I :
finType) (
A :
pred I) (
x :
R) :
+
\prod_(i in A) x = x ^+ #|A|.
-
Lemma prodrXr x I r P (
F :
I → nat) :
-
\prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).
+
Lemma prodrXr x I r P (
F :
I → nat) :
+
\prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).
-
Lemma prodrN (
I :
finType) (
A :
pred I) (
F :
I → R) :
-
\prod_(i in A) - F i = (- 1
) ^+ #|A| × \prod_(i in A) F i.
+
Lemma prodrN (
I :
finType) (
A :
pred I) (
F :
I → R) :
+
\prod_(i in A) - F i = (- 1
) ^+ #|A| × \prod_(i in A) F i.
-
Lemma prodrMn n (
I :
finType) (
A :
pred I) (
F :
I → R) :
-
\prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
+
Lemma prodrMn n (
I :
finType) (
A :
pred I) (
F :
I → R) :
+
\prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
-
Lemma natr_prod I r P (
F :
I → nat) :
-
(\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.
+
Lemma natr_prod I r P (
F :
I → nat) :
+
(\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.
Lemma exprDn_comm x y n (
cxy :
comm x y) :
-
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
+
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma exprBn_comm x y n (
cxy :
comm x y) :
-
(x - y) ^+ n =
-
\sum_(i < n.+1) ((-1
) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
+
(x - y) ^+ n =
+
\sum_(i < n.+1) ((-1
) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma subrXX_comm x y n (
cxy :
comm x y) :
-
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
+
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
-
Lemma exprD1n x n :
(x + 1
) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).
+
Lemma exprD1n x n :
(x + 1
) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).
-
Lemma subrX1 x n :
x ^+ n - 1
= (x - 1
) × (\sum_(i < n) x ^+ i).
+
Lemma subrX1 x n :
x ^+ n - 1
= (x - 1
) × (\sum_(i < n) x ^+ i).
-
Lemma sqrrD1 x :
(x + 1
) ^+ 2
= x ^+ 2
+ x *+ 2
+ 1.
+
Lemma sqrrD1 x :
(x + 1
) ^+ 2
= x ^+ 2
+ x *+ 2
+ 1.
-
Lemma sqrrB1 x :
(x - 1
) ^+ 2
= x ^+ 2
- x *+ 2
+ 1.
+
Lemma sqrrB1 x :
(x - 1
) ^+ 2
= x ^+ 2
- x *+ 2
+ 1.
-
Lemma subr_sqr_1 x :
x ^+ 2
- 1
= (x - 1
) × (x + 1
).
+
Lemma subr_sqr_1 x :
x ^+ 2
- 1
= (x - 1
) × (x + 1
).
-
Definition Frobenius_aut p of p \in [char R] :=
fun x ⇒
x ^+ p.
+
Definition Frobenius_aut p of p \in [char R] :=
fun x ⇒
x ^+ p.
Section FrobeniusAutomorphism.
-
Variable p :
nat.
-
Hypothesis charFp :
p \in [char R].
+
Variable p :
nat.
+
Hypothesis charFp :
p \in [char R].
-
Lemma charf0 :
p%:R = 0
:> R.
+
Lemma charf0 :
p%:R = 0
:> R.
Lemma charf_prime :
prime p.
-
Hint Resolve charf_prime.
+
Hint Resolve charf_prime :
core.
-
Lemma mulrn_char x :
x *+ p = 0.
+
Lemma mulrn_char x :
x *+ p = 0.
-
Lemma natr_mod_char n :
(n %% p)%:R = n%:R :> R.
+
Lemma natr_mod_char n :
(n %% p)%:R = n%:R :> R.
-
Lemma dvdn_charf n : (
p %| n)%
N = (n%:R == 0
:> R).
+
Lemma dvdn_charf n : (
p %| n)%
N = (n%:R == 0
:> R).
-
Lemma charf_eq :
[char R] =i (p : nat_pred).
+
Lemma charf_eq :
[char R] =i (p : nat_pred).
-
Lemma bin_lt_charf_0 k : 0
< k < p → 'C(p, k)%:R = 0
:> R.
+
Lemma bin_lt_charf_0 k : 0
< k < p → 'C(p, k)%:R = 0
:> R.
-
Lemma Frobenius_autE x :
x^f = x ^+ p.
+
Lemma Frobenius_autE x :
x^f = x ^+ p.
-
Lemma Frobenius_aut0 : 0
^f = 0.
+
Lemma Frobenius_aut0 : 0
^f = 0.
-
Lemma Frobenius_aut1 : 1
^f = 1.
+
Lemma Frobenius_aut1 : 1
^f = 1.
-
Lemma Frobenius_autD_comm x y (
cxy :
comm x y) :
(x + y)^f = x^f + y^f.
+
Lemma Frobenius_autD_comm x y (
cxy :
comm x y) :
(x + y)^f = x^f + y^f.
-
Lemma Frobenius_autMn x n :
(x *+ n)^f = x^f *+ n.
+
Lemma Frobenius_autMn x n :
(x *+ n)^f = x^f *+ n.
-
Lemma Frobenius_aut_nat n :
(n%:R)^f = n%:R.
+
Lemma Frobenius_aut_nat n :
(n%:R)^f = n%:R.
-
Lemma Frobenius_autM_comm x y :
comm x y → (x × y)^f = x^f × y^f.
+
Lemma Frobenius_autM_comm x y :
comm x y → (x × y)^f = x^f × y^f.
-
Lemma Frobenius_autX x n :
(x ^+ n)^f = x^f ^+ n.
+
Lemma Frobenius_autX x n :
(x ^+ n)^f = x^f ^+ n.
-
Lemma Frobenius_autN x :
(- x)^f = - x^f.
+
Lemma Frobenius_autN x :
(- x)^f = - x^f.
-
Lemma Frobenius_autB_comm x y :
comm x y → (x - y)^f = x^f - y^f.
+
Lemma Frobenius_autB_comm x y :
comm x y → (x - y)^f = x^f - y^f.
End FrobeniusAutomorphism.
-
Lemma exprNn_char x n :
[char R].-nat n → (- x) ^+ n = - (x ^+ n).
+
Lemma exprNn_char x n :
[char R].-nat n → (- x) ^+ n = - (x ^+ n).
Section Char2.
-
Hypothesis charR2 : 2
\in [char R].
+
Hypothesis charR2 : 2
\in [char R].
-
Lemma addrr_char2 x :
x + x = 0.
+
Lemma addrr_char2 x :
x + x = 0.
-
Lemma oppr_char2 x :
- x = x.
+
Lemma oppr_char2 x :
- x = x.
-
Lemma subr_char2 x y :
x - y = x + y.
+
Lemma subr_char2 x y :
x - y = x + y.
-
Lemma addrK_char2 x :
involutive (
+%R^~ x).
+
Lemma addrK_char2 x :
involutive (
+%R^~ x).
-
Lemma addKr_char2 x :
involutive (
+%R x).
+
Lemma addKr_char2 x :
involutive (
+%R x).
End Char2.
-
Canonical converse_eqType :=
[eqType of R^c].
-
Canonical converse_choiceType :=
[choiceType of R^c].
-
Canonical converse_zmodType :=
[zmodType of R^c].
+
Canonical converse_eqType :=
[eqType of R^c].
+
Canonical converse_choiceType :=
[choiceType of R^c].
+
Canonical converse_zmodType :=
[zmodType of R^c].
Definition converse_ringMixin :=
-
let mul' x y :=
y × x in
-
let mulrA' x y z :=
esym (
mulrA z y x)
in
+
let mul' x y :=
y × x in
+
let mulrA' x y z :=
esym (
mulrA z y x)
in
let mulrDl' x y z :=
mulrDr z x y in
let mulrDr' x y z :=
mulrDl y z x in
@
Ring.Mixin converse_zmodType
1
mul' mulrA' mulr1 mul1r mulrDl' mulrDr' oner_neq0.
-
Canonical converse_ringType :=
RingType R^c converse_ringMixin.
+
Canonical converse_ringType :=
RingType R^c converse_ringMixin.
Section ClosedPredicates.
-
Variable S :
predPredType R.
+
Variable S :
{pred R}.
-
Definition mulr_2closed :=
{in S &, ∀ u v,
u × v \in S}.
-
Definition mulr_closed := 1
\in S ∧ mulr_2closed.
-
Definition smulr_closed := -1
\in S ∧ mulr_2closed.
-
Definition semiring_closed :=
addr_closed S ∧ mulr_closed.
-
Definition subring_closed :=
[/\ 1
\in S, subr_2closed S & mulr_2closed].
+
Definition mulr_2closed :=
{in S &, ∀ u v,
u × v \in S}.
+
Definition mulr_closed := 1
\in S ∧ mulr_2closed.
+
Definition smulr_closed := -1
\in S ∧ mulr_2closed.
+
Definition semiring_closed :=
addr_closed S ∧ mulr_closed.
+
Definition subring_closed :=
[/\ 1
\in S, subr_2closed S & mulr_2closed].
-
Lemma smulr_closedM :
smulr_closed → mulr_closed.
+
Lemma smulr_closedM :
smulr_closed → mulr_closed.
-
Lemma smulr_closedN :
smulr_closed → oppr_closed S.
+
Lemma smulr_closedN :
smulr_closed → oppr_closed S.
-
Lemma semiring_closedD :
semiring_closed → addr_closed S.
+
Lemma semiring_closedD :
semiring_closed → addr_closed S.
-
Lemma semiring_closedM :
semiring_closed → mulr_closed.
+
Lemma semiring_closedM :
semiring_closed → mulr_closed.
-
Lemma subring_closedB :
subring_closed → zmod_closed S.
+
Lemma subring_closedB :
subring_closed → zmod_closed S.
-
Lemma subring_closedM :
subring_closed → smulr_closed.
+
Lemma subring_closedM :
subring_closed → smulr_closed.
-
Lemma subring_closed_semi :
subring_closed → semiring_closed.
+
Lemma subring_closed_semi :
subring_closed → semiring_closed.
End ClosedPredicates.
@@ -1474,28 +1490,28 @@
Let Rc :=
converse_ringType R.
-
Lemma mulIr_eq0 x y :
rreg x → (y × x == 0
) = (y == 0
).
+
Lemma mulIr_eq0 x y :
rreg x → (y × x == 0
) = (y == 0
).
-
Lemma mulIr0_rreg x :
(∀ y,
y × x = 0
→ y = 0
) → rreg x.
+
Lemma mulIr0_rreg x :
(∀ y,
y × x = 0
→ y = 0
) → rreg x.
-
Lemma rreg_neq0 x :
rreg x → x != 0.
+
Lemma rreg_neq0 x :
rreg x → x != 0.
-
Lemma rregN x :
rreg x → rreg (
- x).
+
Lemma rregN x :
rreg x → rreg (
- x).
-
Lemma rreg1 :
rreg (1
: R).
+
Lemma rreg1 :
rreg (1
: R).
-
Lemma rregM x y :
rreg x → rreg y → rreg (
x × y).
+
Lemma rregM x y :
rreg x → rreg y → rreg (
x × y).
-
Lemma revrX x n :
(x : Rc) ^+ n = (x : R) ^+ n.
+
Lemma revrX x n :
(x : Rc) ^+ n = (x : R) ^+ n.
-
Lemma rregX x n :
rreg x → rreg (
x ^+ n).
+
Lemma rregX x n :
rreg x → rreg (
x ^+ n).
End RightRegular.
@@ -1505,11 +1521,11 @@
Structure mixin_of (
R :
ringType) (
V :
zmodType) :
Type :=
Mixin {
-
scale :
R → V → V;
-
_ :
∀ a b v,
scale a (
scale b v)
= scale (
a × b)
v;
-
_ :
left_id 1
scale;
-
_ :
right_distributive scale +%R;
-
_ :
∀ v,
{morph scale^~ v: a b / a + b}
+
scale :
R → V → V;
+
_ :
∀ a b v,
scale a (
scale b v)
= scale (
a × b)
v;
+
_ :
left_id 1
scale;
+
_ :
right_distributive scale +%R;
+
_ :
∀ v,
{morph scale^~ v: a b / a + b}
}.
@@ -1521,26 +1537,26 @@
Structure class_of V :=
Class {
base :
Zmodule.class_of V;
-
mixin :
mixin_of R (
Zmodule.Pack base V)
+
mixin :
mixin_of R (
Zmodule.Pack base)
}.
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack phR T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack phR T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack b0 (
m0 :
mixin_of R (@
Zmodule.Pack T b0 T)) :=
-
fun bT b &
phant_id (
Zmodule.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack phR (@
Class T b m)
T.
+
Definition pack b0 (
m0 :
mixin_of R (@
Zmodule.Pack T b0)) :=
+
fun bT b &
phant_id (
Zmodule.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack phR (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
End ClassDef.
@@ -1556,12 +1572,12 @@
Canonical choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical zmodType.
-
Notation lmodType R := (
type (
Phant R)).
-
Notation LmodType R T m := (@
pack _ (
Phant R)
T _ m _ _ id _ id).
+
Notation lmodType R := (
type (
Phant R)).
+
Notation LmodType R T m := (@
pack _ (
Phant R)
T _ m _ _ id _ id).
Notation LmodMixin :=
Mixin.
-
Notation "[ 'lmodType' R 'of' T 'for' cT ]" := (@
clone _ (
Phant R)
T cT _ idfun)
+
Notation "[ 'lmodType' R 'of' T 'for' cT ]" := (@
clone _ (
Phant R)
T cT _ idfun)
(
at level 0,
format "[ 'lmodType' R 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'lmodType' R 'of' T ]" := (@
clone _ (
Phant R)
T _ _ id)
+
Notation "[ 'lmodType' R 'of' T ]" := (@
clone _ (
Phant R)
T _ _ id)
(
at level 0,
format "[ 'lmodType' R 'of' T ]") :
form_scope.
End Exports.
@@ -1585,80 +1601,80 @@
-
Lemma scalerA a b v :
a *: (b *: v) = a × b *: v.
+
Lemma scalerA a b v :
a *: (b *: v) = a × b *: v.
-
Lemma scale1r : @
left_id R V 1
*:%R.
+
Lemma scale1r : @
left_id R V 1
*:%R.
-
Lemma scalerDr a :
{morph *:%R a : u v / u + v}.
+
Lemma scalerDr a :
{morph *:%R a : u v / u + v}.
-
Lemma scalerDl v :
{morph *:%R^~ v : a b / a + b}.
+
Lemma scalerDl v :
{morph *:%R^~ v : a b / a + b}.
-
Lemma scale0r v : 0
*: v = 0.
+
Lemma scale0r v : 0
*: v = 0.
-
Lemma scaler0 a :
a *: 0
= 0
:> V.
+
Lemma scaler0 a :
a *: 0
= 0
:> V.
-
Lemma scaleNr a v :
- a *: v = - (a *: v).
+
Lemma scaleNr a v :
- a *: v = - (a *: v).
-
Lemma scaleN1r v :
(- 1
) *: v = - v.
+
Lemma scaleN1r v :
(- 1
) *: v = - v.
-
Lemma scalerN a v :
a *: (- v) = - (a *: v).
+
Lemma scalerN a v :
a *: (- v) = - (a *: v).
-
Lemma scalerBl a b v :
(a - b) *: v = a *: v - b *: v.
+
Lemma scalerBl a b v :
(a - b) *: v = a *: v - b *: v.
-
Lemma scalerBr a u v :
a *: (u - v) = a *: u - a *: v.
+
Lemma scalerBr a u v :
a *: (u - v) = a *: u - a *: v.
-
Lemma scaler_nat n v :
n%:R *: v = v *+ n.
+
Lemma scaler_nat n v :
n%:R *: v = v *+ n.
-
Lemma scaler_sign (
b :
bool)
v:
(-1
) ^+ b *: v = (if b then - v else v).
+
Lemma scaler_sign (
b :
bool)
v:
(-1
) ^+ b *: v = (if b then - v else v).
-
Lemma signrZK n : @
involutive V (
*:%R ((-1) ^+ n)).
+
Lemma signrZK n : @
involutive V (
*:%R ((-1) ^+ n)).
-
Lemma scalerMnl a v n :
a *: v *+ n = (a *+ n) *: v.
+
Lemma scalerMnl a v n :
a *: v *+ n = (a *+ n) *: v.
-
Lemma scalerMnr a v n :
a *: v *+ n = a *: (v *+ n).
+
Lemma scalerMnr a v n :
a *: v *+ n = a *: (v *+ n).
-
Lemma scaler_suml v I r (
P :
pred I)
F :
-
(\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.
+
Lemma scaler_suml v I r (
P :
pred I)
F :
+
(\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.
-
Lemma scaler_sumr a I r (
P :
pred I) (
F :
I → V) :
-
a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.
+
Lemma scaler_sumr a I r (
P :
pred I) (
F :
I → V) :
+
a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.
Section ClosedPredicates.
-
Variable S :
predPredType V.
+
Variable S :
{pred V}.
-
Definition scaler_closed :=
∀ a,
{in S, ∀ v,
a *: v \in S}.
-
Definition linear_closed :=
∀ a,
{in S &, ∀ u v,
a *: u + v \in S}.
-
Definition submod_closed := 0
\in S ∧ linear_closed.
+
Definition scaler_closed :=
∀ a,
{in S, ∀ v,
a *: v \in S}.
+
Definition linear_closed :=
∀ a,
{in S &, ∀ u v,
a *: u + v \in S}.
+
Definition submod_closed := 0
\in S ∧ linear_closed.
-
Lemma linear_closedB :
linear_closed → subr_2closed S.
+
Lemma linear_closedB :
linear_closed → subr_2closed S.
-
Lemma submod_closedB :
submod_closed → zmod_closed S.
+
Lemma submod_closedB :
submod_closed → zmod_closed S.
-
Lemma submod_closedZ :
submod_closed → scaler_closed.
+
Lemma submod_closedZ :
submod_closed → scaler_closed.
End ClosedPredicates.
@@ -1670,8 +1686,8 @@
Module Lalgebra.
-
Definition axiom (
R :
ringType) (
V :
lmodType R) (
mul :
V → V → V) :=
-
∀ a u v,
a *: mul u v = mul (
a *: u)
v.
+
Definition axiom (
R :
ringType) (
V :
lmodType R) (
mul :
V → V → V) :=
+
∀ a u v,
a *: mul u v = mul (
a *: u)
v.
Section ClassDef.
@@ -1682,33 +1698,33 @@
Record class_of (
T :
Type) :
Type :=
Class {
base :
Ring.class_of T;
-
mixin :
Lmodule.mixin_of R (
Zmodule.Pack base T);
-
ext : @
axiom R (
Lmodule.Pack _ (
Lmodule.Class mixin)
T) (
Ring.mul base)
+
mixin :
Lmodule.mixin_of R (
Zmodule.Pack base);
+
ext : @
axiom R (
Lmodule.Pack _ (
Lmodule.Class mixin)) (
Ring.mul base)
}.
Definition base2 R m :=
Lmodule.Class (@
mixin R m).
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack phR T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack phR T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack T b0 mul0 (
axT : @
axiom R (@
Lmodule.Pack R _ T b0 T)
mul0) :=
-
fun bT b &
phant_id (
Ring.class bT) (
b : Ring.class_of T) ⇒
-
fun mT m &
phant_id (@
Lmodule.class R phR mT) (@
Lmodule.Class R T b m) ⇒
-
fun ax &
phant_id axT ax ⇒
-
Pack (
Phant R) (@
Class T b m ax)
T.
+
Definition pack T b0 mul0 (
axT : @
axiom R (@
Lmodule.Pack R _ T b0)
mul0) :=
+
fun bT b &
phant_id (
Ring.class bT) (
b : Ring.class_of T) ⇒
+
fun mT m &
phant_id (@
Lmodule.class R phR mT) (@
Lmodule.Class R T b m) ⇒
+
fun ax &
phant_id axT ax ⇒
+
Pack (
Phant R) (@
Class T b m ax).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition lmodType := @
Lmodule.Pack R phR cT xclass xT.
-
Definition lmod_ringType := @
Lmodule.Pack R phR ringType xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition lmodType := @
Lmodule.Pack R phR cT xclass.
+
Definition lmod_ringType := @
Lmodule.Pack R phR ringType xclass.
End ClassDef.
@@ -1729,12 +1745,12 @@
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Canonical lmod_ringType.
-
Notation lalgType R := (
type (
Phant R)).
-
Notation LalgType R T a := (@
pack _ (
Phant R)
T _ _ a _ _ id _ _ id _ id).
-
Notation "[ 'lalgType' R 'of' T 'for' cT ]" := (@
clone _ (
Phant R)
T cT _ idfun)
+
Notation lalgType R := (
type (
Phant R)).
+
Notation LalgType R T a := (@
pack _ (
Phant R)
T _ _ a _ _ id _ _ id _ id).
+
Notation "[ 'lalgType' R 'of' T 'for' cT ]" := (@
clone _ (
Phant R)
T cT _ idfun)
(
at level 0,
format "[ 'lalgType' R 'of' T 'for' cT ]")
:
form_scope.
-
Notation "[ 'lalgType' R 'of' T ]" := (@
clone _ (
Phant R)
T _ _ id)
+
Notation "[ 'lalgType' R 'of' T ]" := (@
clone _ (
Phant R)
T _ _ id)
(
at level 0,
format "[ 'lalgType' R 'of' T ]") :
form_scope.
End Exports.
@@ -1767,16 +1783,16 @@
Implicit Types x y :
A.
-
Lemma scalerAl k (
x y :
A) :
k *: (x × y) = k *: x × y.
+
Lemma scalerAl k (
x y :
A) :
k *: (x × y) = k *: x × y.
-
Lemma mulr_algl a x :
a%:A × x = a *: x.
+
Lemma mulr_algl a x :
a%:A × x = a *: x.
-
Canonical regular_eqType :=
[eqType of R^o].
-
Canonical regular_choiceType :=
[choiceType of R^o].
-
Canonical regular_zmodType :=
[zmodType of R^o].
-
Canonical regular_ringType :=
[ringType of R^o].
+
Canonical regular_eqType :=
[eqType of R^o].
+
Canonical regular_choiceType :=
[choiceType of R^o].
+
Canonical regular_zmodType :=
[zmodType of R^o].
+
Canonical regular_ringType :=
[ringType of R^o].
Definition regular_lmodMixin :=
@@ -1784,23 +1800,23 @@
mkMixin (@
mulrA R) (@
mul1r R) (@
mulrDr R) (
fun v a b ⇒
mulrDl a b v).
-
Canonical regular_lmodType :=
LmodType R R^o regular_lmodMixin.
-
Canonical regular_lalgType :=
LalgType R R^o (@
mulrA regular_ringType).
+
Canonical regular_lmodType :=
LmodType R R^o regular_lmodMixin.
+
Canonical regular_lalgType :=
LalgType R R^o (@
mulrA regular_ringType).
Section ClosedPredicates.
-
Variable S :
predPredType A.
+
Variable S :
{pred A}.
-
Definition subalg_closed :=
[/\ 1
\in S, linear_closed S & mulr_2closed S].
+
Definition subalg_closed :=
[/\ 1
\in S, linear_closed S & mulr_2closed S].
-
Lemma subalg_closedZ :
subalg_closed → submod_closed S.
+
Lemma subalg_closedZ :
subalg_closed → submod_closed S.
-
Lemma subalg_closedBM :
subalg_closed → subring_closed S.
+
Lemma subalg_closedBM :
subalg_closed → subring_closed S.
End ClosedPredicates.
@@ -1826,15 +1842,15 @@
Variables U V :
zmodType.
-
Definition axiom (
f :
U → V) :=
{morph f : x y / x - y}.
+
Definition axiom (
f :
U → V) :=
{morph f : x y / x - y}.
-
Structure map (
phUV :
phant (
U → V)) :=
Pack {
apply;
_ :
axiom apply}.
+
Structure map (
phUV :
phant (
U → V)) :=
Pack {
apply;
_ :
axiom apply}.
-
Variables (
phUV :
phant (
U → V)) (
f g :
U → V) (
cF :
map phUV).
+
Variables (
phUV :
phant (
U → V)) (
f g :
U → V) (
cF :
map phUV).
Definition class :=
let:
Pack _ c as cF' :=
cF return axiom cF' in c.
-
Definition clone fA of phant_id g (
apply cF) &
phant_id fA class :=
+
Definition clone fA of phant_id g (
apply cF) &
phant_id fA class :=
@
Pack phUV f fA.
@@ -1844,12 +1860,12 @@
Module Exports.
Notation additive f := (
axiom f).
Coercion apply : map >-> Funclass.
-
Notation Additive fA := (
Pack (
Phant _)
fA).
-
Notation "{ 'additive' fUV }" := (
map (
Phant fUV))
+
Notation Additive fA := (
Pack (
Phant _)
fA).
+
Notation "{ 'additive' fUV }" := (
map (
Phant fUV))
(
at level 0,
format "{ 'additive' fUV }") :
ring_scope.
-
Notation "[ 'additive' 'of' f 'as' g ]" := (@
clone _ _ _ f g _ _ idfun id)
+
Notation "[ 'additive' 'of' f 'as' g ]" := (@
clone _ _ _ f g _ _ idfun id)
(
at level 0,
format "[ 'additive' 'of' f 'as' g ]") :
form_scope.
-
Notation "[ 'additive' 'of' f ]" := (@
clone _ _ _ f f _ _ id id)
+
Notation "[ 'additive' 'of' f ]" := (@
clone _ _ _ f f _ _ id id)
(
at level 0,
format "[ 'additive' 'of' f ]") :
form_scope.
End Exports.
@@ -1866,9 +1882,9 @@
Section LiftedZmod.
Variables (
U :
Type) (
V :
zmodType).
-
Definition null_fun_head (
phV :
phant V)
of U :
V :=
let:
Phant :=
phV in 0.
-
Definition add_fun_head t (
f g :
U → V)
x :=
let:
tt :=
t in f x + g x.
-
Definition sub_fun_head t (
f g :
U → V)
x :=
let:
tt :=
t in f x - g x.
+
Definition null_fun_head (
phV :
phant V)
of U :
V :=
let:
Phant :=
phV in 0.
+
Definition add_fun_head t (
f g :
U → V)
x :=
let:
tt :=
t in f x + g x.
+
Definition sub_fun_head t (
f g :
U → V)
x :=
let:
tt :=
t in f x - g x.
End LiftedZmod.
@@ -1880,9 +1896,9 @@
Section LiftedRing.
Variables (
R :
ringType) (
T :
Type).
-
Implicit Type f :
T → R.
-
Definition mull_fun_head t a f x :=
let:
tt :=
t in a × f x.
-
Definition mulr_fun_head t a f x :=
let:
tt :=
t in f x × a.
+
Implicit Type f :
T → R.
+
Definition mull_fun_head t a f x :=
let:
tt :=
t in a × f x.
+
Definition mulr_fun_head t a f x :=
let:
tt :=
t in f x × a.
End LiftedRing.
@@ -1894,12 +1910,12 @@
@@ -1917,42 +1933,42 @@
Section Properties.
-
Variables (
U V :
zmodType) (
k :
unit) (
f :
{additive U → V}).
+
Variables (
U V :
zmodType) (
k :
unit) (
f :
{additive U → V}).
-
Lemma raddfB :
{morph f : x y / x - y}.
+
Lemma raddfB :
{morph f : x y / x - y}.
-
Lemma raddf0 :
f 0
= 0.
+
Lemma raddf0 :
f 0
= 0.
-
Lemma raddf_eq0 x :
injective f → (f x == 0
) = (x == 0
).
+
Lemma raddf_eq0 x :
injective f → (f x == 0
) = (x == 0
).
-
Lemma raddfN :
{morph f : x / - x}.
+
Lemma raddfN :
{morph f : x / - x}.
-
Lemma raddfD :
{morph f : x y / x + y}.
+
Lemma raddfD :
{morph f : x y / x + y}.
-
Lemma raddfMn n :
{morph f : x / x *+ n}.
+
Lemma raddfMn n :
{morph f : x / x *+ n}.
-
Lemma raddfMNn n :
{morph f : x / x *- n}.
+
Lemma raddfMNn n :
{morph f : x / x *- n}.
-
Lemma raddf_sum I r (
P :
pred I)
E :
-
f (
\sum_(i <- r | P i) E i)
= \sum_(i <- r | P i) f (
E i).
+
Lemma raddf_sum I r (
P :
pred I)
E :
+
f (
\sum_(i <- r | P i) E i)
= \sum_(i <- r | P i) f (
E i).
-
Lemma can2_additive f' :
cancel f f' → cancel f' f → additive f'.
+
Lemma can2_additive f' :
cancel f f' → cancel f' f → additive f'.
Lemma bij_additive :
-
bijective f → exists2 f' : {additive V → U}, cancel f f' & cancel f' f.
+
bijective f → exists2 f' : {additive V → U}, cancel f f' & cancel f' f.
-
Fact locked_is_additive :
additive (
locked_with k (
f : U → V)).
+
Fact locked_is_additive :
additive (
locked_with k (
f : U → V)).
Canonical locked_additive :=
Additive locked_is_additive.
@@ -1962,22 +1978,22 @@
Section RingProperties.
-
Variables (
R S :
ringType) (
f :
{additive R → S}).
+
Variables (
R S :
ringType) (
f :
{additive R → S}).
-
Lemma raddfMnat n x :
f (
n%:R × x)
= n%:R × f x.
+
Lemma raddfMnat n x :
f (
n%:R × x)
= n%:R × f x.
-
Lemma raddfMsign n x :
f (
(-1
) ^+ n × x)
= (-1
) ^+ n × f x.
+
Lemma raddfMsign n x :
f (
(-1
) ^+ n × x)
= (-1
) ^+ n × f x.
-
Variables (
U :
lmodType R) (
V :
lmodType S) (
h :
{additive U → V}).
+
Variables (
U :
lmodType R) (
V :
lmodType S) (
h :
{additive U → V}).
-
Lemma raddfZnat n u :
h (
n%:R *: u)
= n%:R *: h u.
+
Lemma raddfZnat n u :
h (
n%:R *: u)
= n%:R *: h u.
-
Lemma raddfZsign n u :
h (
(-1
) ^+ n *: u)
= (-1
) ^+ n *: h u.
+
Lemma raddfZsign n u :
h (
(-1
) ^+ n *: u)
= (-1
) ^+ n *: h u.
End RingProperties.
@@ -1986,30 +2002,30 @@
Section AddFun.
-
Variables (
U V W :
zmodType) (
f g :
{additive V → W}) (
h :
{additive U → V}).
+
Variables (
U V W :
zmodType) (
f g :
{additive V → W}) (
h :
{additive U → V}).
-
Fact idfun_is_additive :
additive (
@idfun U).
+
Fact idfun_is_additive :
additive (
@idfun U).
Canonical idfun_additive :=
Additive idfun_is_additive.
-
Fact comp_is_additive :
additive (
f \o h).
+
Fact comp_is_additive :
additive (
f \o h).
Canonical comp_additive :=
Additive comp_is_additive.
-
Fact opp_is_additive :
additive (
-%R : U → U).
+
Fact opp_is_additive :
additive (
-%R : U → U).
Canonical opp_additive :=
Additive opp_is_additive.
-
Fact null_fun_is_additive :
additive (
\0 : U → V).
+
Fact null_fun_is_additive :
additive (
\0 : U → V).
Canonical null_fun_additive :=
Additive null_fun_is_additive.
-
Fact add_fun_is_additive :
additive (
f \+ g).
+
Fact add_fun_is_additive :
additive (
f \+ g).
Canonical add_fun_additive :=
Additive add_fun_is_additive.
-
Fact sub_fun_is_additive :
additive (
f \- g).
+
Fact sub_fun_is_additive :
additive (
f \- g).
Canonical sub_fun_additive :=
Additive sub_fun_is_additive.
@@ -2020,14 +2036,14 @@
Variables (
R :
ringType) (
U :
zmodType).
-
Variables (
a :
R) (
f :
{additive U → R}).
+
Variables (
a :
R) (
f :
{additive U → R}).
-
Fact mull_fun_is_additive :
additive (
a \*o f).
+
Fact mull_fun_is_additive :
additive (
a \*o f).
Canonical mull_fun_additive :=
Additive mull_fun_is_additive.
-
Fact mulr_fun_is_additive :
additive (
a \o× f).
+
Fact mulr_fun_is_additive :
additive (
a \o× f).
Canonical mulr_fun_additive :=
Additive mulr_fun_is_additive.
@@ -2038,11 +2054,11 @@
Variables (
R :
ringType) (
U :
zmodType) (
V :
lmodType R).
-
Variables (
a :
R) (
f :
{additive U → V}).
+
Variables (
a :
R) (
f :
{additive U → V}).
Canonical scale_additive :=
Additive (@
scalerBr R V a).
-
Canonical scale_fun_additive :=
[additive of a \*: f as f \; *:%R a].
+
Canonical scale_fun_additive :=
[additive of a \*: f as f \; *:%R a].
End ScaleFun.
@@ -2060,26 +2076,26 @@
Variables R S :
ringType.
-
Definition mixin_of (
f :
R → S) :=
-
{morph f : x y / x × y}%
R × (f 1
= 1
) : Prop.
+
Definition mixin_of (
f :
R → S) :=
+
{morph f : x y / x × y}%
R × (f 1
= 1
) : Prop.
Record class_of f :
Prop :=
Class {
base :
additive f;
mixin :
mixin_of f}.
-
Structure map (
phRS :
phant (
R → S)) :=
Pack {
apply;
_ :
class_of apply}.
-
Variables (
phRS :
phant (
R → S)) (
f g :
R → S) (
cF :
map phRS).
+
Structure map (
phRS :
phant (
R → S)) :=
Pack {
apply;
_ :
class_of apply}.
+
Variables (
phRS :
phant (
R → S)) (
f g :
R → S) (
cF :
map phRS).
Definition class :=
let:
Pack _ c as cF' :=
cF return class_of cF' in c.
-
Definition clone fM of phant_id g (
apply cF) &
phant_id fM class :=
+
Definition clone fM of phant_id g (
apply cF) &
phant_id fM class :=
@
Pack phRS f fM.
Definition pack (
fM :
mixin_of f) :=
-
fun (
bF :
Additive.map phRS)
fA &
phant_id (
Additive.class bF)
fA ⇒
+
fun (
bF :
Additive.map phRS)
fA &
phant_id (
Additive.class bF)
fA ⇒
Pack phRS (
Class fA fM).
@@ -2095,13 +2111,13 @@
Coercion base : rmorphism >-> Additive.axiom.
Coercion mixin : rmorphism >-> multiplicative.
Coercion apply : map >-> Funclass.
-
Notation RMorphism fM := (
Pack (
Phant _)
fM).
-
Notation AddRMorphism fM := (
pack fM id).
-
Notation "{ 'rmorphism' fRS }" := (
map (
Phant fRS))
+
Notation RMorphism fM := (
Pack (
Phant _)
fM).
+
Notation AddRMorphism fM := (
pack fM id).
+
Notation "{ 'rmorphism' fRS }" := (
map (
Phant fRS))
(
at level 0,
format "{ 'rmorphism' fRS }") :
ring_scope.
-
Notation "[ 'rmorphism' 'of' f 'as' g ]" := (@
clone _ _ _ f g _ _ idfun id)
+
Notation "[ 'rmorphism' 'of' f 'as' g ]" := (@
clone _ _ _ f g _ _ idfun id)
(
at level 0,
format "[ 'rmorphism' 'of' f 'as' g ]") :
form_scope.
-
Notation "[ 'rmorphism' 'of' f ]" := (@
clone _ _ _ f f _ _ id id)
+
Notation "[ 'rmorphism' 'of' f ]" := (@
clone _ _ _ f f _ _ id id)
(
at level 0,
format "[ 'rmorphism' 'of' f ]") :
form_scope.
Coercion additive : map >-> Additive.map.
Canonical additive.
@@ -2118,57 +2134,57 @@
Section Properties.
-
Variables (
R S :
ringType) (
k :
unit) (
f :
{rmorphism R → S}).
+
Variables (
R S :
ringType) (
k :
unit) (
f :
{rmorphism R → S}).
-
Lemma rmorph0 :
f 0
= 0.
-
Lemma rmorphN :
{morph f : x / - x}.
-
Lemma rmorphD :
{morph f : x y / x + y}.
-
Lemma rmorphB :
{morph f: x y / x - y}.
-
Lemma rmorphMn n :
{morph f : x / x *+ n}.
-
Lemma rmorphMNn n :
{morph f : x / x *- n}.
-
Lemma rmorph_sum I r (
P :
pred I)
E :
-
f (
\sum_(i <- r | P i) E i)
= \sum_(i <- r | P i) f (
E i).
-
Lemma rmorphMsign n :
{morph f : x / (- 1
) ^+ n × x}.
+
Lemma rmorph0 :
f 0
= 0.
+
Lemma rmorphN :
{morph f : x / - x}.
+
Lemma rmorphD :
{morph f : x y / x + y}.
+
Lemma rmorphB :
{morph f: x y / x - y}.
+
Lemma rmorphMn n :
{morph f : x / x *+ n}.
+
Lemma rmorphMNn n :
{morph f : x / x *- n}.
+
Lemma rmorph_sum I r (
P :
pred I)
E :
+
f (
\sum_(i <- r | P i) E i)
= \sum_(i <- r | P i) f (
E i).
+
Lemma rmorphMsign n :
{morph f : x / (- 1
) ^+ n × x}.
Lemma rmorphismP :
rmorphism f.
Lemma rmorphismMP :
multiplicative f.
-
Lemma rmorph1 :
f 1
= 1.
-
Lemma rmorphM :
{morph f: x y / x × y}.
+
Lemma rmorph1 :
f 1
= 1.
+
Lemma rmorphM :
{morph f: x y / x × y}.
-
Lemma rmorph_prod I r (
P :
pred I)
E :
-
f (
\prod_(i <- r | P i) E i)
= \prod_(i <- r | P i) f (
E i).
+
Lemma rmorph_prod I r (
P :
pred I)
E :
+
f (
\prod_(i <- r | P i) E i)
= \prod_(i <- r | P i) f (
E i).
-
Lemma rmorphX n :
{morph f: x / x ^+ n}.
+
Lemma rmorphX n :
{morph f: x / x ^+ n}.
-
Lemma rmorph_nat n :
f n%:R = n%:R.
-
Lemma rmorphN1 :
f (- 1)
= (- 1
).
+
Lemma rmorph_nat n :
f n%:R = n%:R.
+
Lemma rmorphN1 :
f (- 1)
= (- 1
).
-
Lemma rmorph_sign n :
f (
(- 1
) ^+ n)
= (- 1
) ^+ n.
+
Lemma rmorph_sign n :
f (
(- 1
) ^+ n)
= (- 1
) ^+ n.
-
Lemma rmorph_char p :
p \in [char R] → p \in [char S].
+
Lemma rmorph_char p :
p \in [char R] → p \in [char S].
-
Lemma rmorph_eq_nat x n :
injective f → (f x == n%:R) = (x == n%:R).
+
Lemma rmorph_eq_nat x n :
injective f → (f x == n%:R) = (x == n%:R).
-
Lemma rmorph_eq1 x :
injective f → (f x == 1
) = (x == 1
).
+
Lemma rmorph_eq1 x :
injective f → (f x == 1
) = (x == 1
).
-
Lemma can2_rmorphism f' :
cancel f f' → cancel f' f → rmorphism f'.
+
Lemma can2_rmorphism f' :
cancel f f' → cancel f' f → rmorphism f'.
Lemma bij_rmorphism :
-
bijective f → exists2 f' : {rmorphism S → R}, cancel f f' & cancel f' f.
+
bijective f → exists2 f' : {rmorphism S → R}, cancel f f' & cancel f' f.
-
Fact locked_is_multiplicative :
multiplicative (
locked_with k (
f : R → S)).
+
Fact locked_is_multiplicative :
multiplicative (
locked_with k (
f : R → S)).
Canonical locked_rmorphism :=
AddRMorphism locked_is_multiplicative.
@@ -2178,14 +2194,14 @@
Section Projections.
-
Variables (
R S T :
ringType) (
f :
{rmorphism S → T}) (
g :
{rmorphism R → S}).
+
Variables (
R S T :
ringType) (
f :
{rmorphism S → T}) (
g :
{rmorphism R → S}).
-
Fact idfun_is_multiplicative :
multiplicative (
@idfun R).
+
Fact idfun_is_multiplicative :
multiplicative (
@idfun R).
Canonical idfun_rmorphism :=
AddRMorphism idfun_is_multiplicative.
-
Fact comp_is_multiplicative :
multiplicative (
f \o g).
+
Fact comp_is_multiplicative :
multiplicative (
f \o g).
Canonical comp_rmorphism :=
AddRMorphism comp_is_multiplicative.
@@ -2203,7 +2219,7 @@
Canonical in_alg_rmorphism :=
RMorphism in_alg_is_rmorphism.
-
Lemma in_algE a :
in_alg_loc A a = a%:A.
+
Lemma in_algE a :
in_alg_loc A a = a%:A.
End InAlgebra.
@@ -2218,31 +2234,31 @@
Section ScaleLaw.
-
Structure law (
R :
ringType) (
V :
zmodType) (
s :
R → V → V) :=
Law {
-
op :
R → V → V;
-
_ :
op = s;
-
_ :
op (-1)
=1 -%R;
+
Structure law (
R :
ringType) (
V :
zmodType) (
s :
R → V → V) :=
Law {
+
op :
R → V → V;
+
_ :
op = s;
+
_ :
op (-1)
=1 -%R;
_ :
∀ a,
additive (
op a)
}.
-
Definition mul_law R :=
Law (
erefl *%R) (@
mulN1r R) (@
mulrBr R).
-
Definition scale_law R U :=
Law (
erefl *:%R) (@
scaleN1r R U) (@
scalerBr R U).
+
Definition mul_law R :=
Law (
erefl *%R) (@
mulN1r R) (@
mulrBr R).
+
Definition scale_law R U :=
Law (
erefl *:%R) (@
scaleN1r R U) (@
scalerBr R U).
-
Variables (
R :
ringType) (
V :
zmodType) (
s :
R → V → V) (
s_law :
law s).
+
Variables (
R :
ringType) (
V :
zmodType) (
s :
R → V → V) (
s_law :
law s).
-
Lemma opE :
s_op = s.
-
Lemma N1op :
s_op (-1)
=1 -%R.
+
Lemma opE :
s_op = s.
+
Lemma N1op :
s_op (-1)
=1 -%R.
Fact opB a :
additive (
s_op a).
Definition op_additive a :=
Additive (
opB a).
-
Variables (
aR :
ringType) (
nu :
{rmorphism aR → R}).
-
Fact comp_opE :
nu \; s_op = nu \; s.
-
Fact compN1op : (
nu \; s_op) (-1)
=1 -%R.
-
Definition comp_law :
law (
nu \; s) :=
Law comp_opE compN1op (
fun a ⇒
opB _).
+
Variables (
aR :
ringType) (
nu :
{rmorphism aR → R}).
+
Fact comp_opE :
nu \; s_op = nu \; s.
+
Fact compN1op : (
nu \; s_op) (-1)
=1 -%R.
+
Definition comp_law :
law (
nu \; s) :=
Law comp_opE compN1op (
fun a ⇒
opB _).
End ScaleLaw.
@@ -2257,33 +2273,33 @@
Section ClassDef.
-
Variables (
R :
ringType) (
U :
lmodType R) (
V :
zmodType) (
s :
R → V → V).
-
Implicit Type phUV :
phant (
U → V).
+
Variables (
R :
ringType) (
U :
lmodType R) (
V :
zmodType) (
s :
R → V → V).
+
Implicit Type phUV :
phant (
U → V).
-
Definition axiom (
f :
U → V) (
s_law :
Scale.law s)
of s = s_law :=
-
∀ a,
{morph f : u v / a *: u + v >-> s a u + v}.
-
Definition mixin_of (
f :
U → V) :=
-
∀ a,
{morph f : v / a *: v >-> s a v}.
+
Definition axiom (
f :
U → V) (
s_law :
Scale.law s)
of s = s_law :=
+
∀ a,
{morph f : u v / a *: u + v >-> s a u + v}.
+
Definition mixin_of (
f :
U → V) :=
+
∀ a,
{morph f : v / a *: v >-> s a v}.
Record class_of f :
Prop :=
Class {
base :
additive f;
mixin :
mixin_of f}.
-
Lemma class_of_axiom f s_law Ds : @
axiom f s_law Ds → class_of f.
+
Lemma class_of_axiom f s_law Ds : @
axiom f s_law Ds → class_of f.
-
Structure map (
phUV :
phant (
U → V)) :=
Pack {
apply;
_ :
class_of apply}.
+
Structure map (
phUV :
phant (
U → V)) :=
Pack {
apply;
_ :
class_of apply}.
-
Variables (
phUV :
phant (
U → V)) (
f g :
U → V) (
cF :
map phUV).
+
Variables (
phUV :
phant (
U → V)) (
f g :
U → V) (
cF :
map phUV).
Definition class :=
let:
Pack _ c as cF' :=
cF return class_of cF' in c.
-
Definition clone fL of phant_id g (
apply cF) &
phant_id fL class :=
+
Definition clone fL of phant_id g (
apply cF) &
phant_id fL class :=
@
Pack phUV f fL.
Definition pack (
fZ :
mixin_of f) :=
-
fun (
bF :
Additive.map phUV)
fA &
phant_id (
Additive.class bF)
fA ⇒
+
fun (
bF :
Additive.map phUV)
fA &
phant_id (
Additive.class bF)
fA ⇒
Pack phUV (
Class fA fZ).
@@ -2296,11 +2312,11 @@
Support for right-to-left rewriting with the generic linearZ rule.
-
Notation mapUV := (
map (
Phant (
U → V))).
+
Notation mapUV := (
map (
Phant (
U → V))).
Definition map_class :=
mapUV.
Definition map_at (
a :
R) :=
mapUV.
-
Structure map_for a s_a :=
MapFor {
map_for_map :
mapUV;
_ :
s a = s_a}.
-
Definition unify_map_at a (
f :
map_at a) :=
MapFor f (
erefl (
s a)).
+
Structure map_for a s_a :=
MapFor {
map_for_map :
mapUV;
_ :
s a = s_a}.
+
Definition unify_map_at a (
f :
map_at a) :=
MapFor f (
erefl (
s a)).
Structure wrapped :=
Wrap {
unwrap :
mapUV}.
Definition wrap (
f :
map_class) :=
Wrap f.
@@ -2314,34 +2330,34 @@
Canonical Scale.comp_law.
Canonical Scale.op_additive.
Delimit Scope linear_ring_scope with linR.
-
Notation "a *: u" := (@
Scale.op _ _ *:%R _ a u) :
linear_ring_scope.
-
Notation "a * u" := (@
Scale.op _ _ *%R _ a u) :
linear_ring_scope.
-
Notation "a *:^ nu u" := (@
Scale.op _ _ (
nu \; *:%R)
_ a u)
+
Notation "a *: u" := (@
Scale.op _ _ *:%R _ a u) :
linear_ring_scope.
+
Notation "a * u" := (@
Scale.op _ _ *%R _ a u) :
linear_ring_scope.
+
Notation "a *:^ nu u" := (@
Scale.op _ _ (
nu \; *:%R)
_ a u)
(
at level 40,
nu at level 1,
format "a *:^ nu u") :
linear_ring_scope.
-
Notation "a *^ nu u" := (@
Scale.op _ _ (
nu \; *%R)
_ a u)
+
Notation "a *^ nu u" := (@
Scale.op _ _ (
nu \; *%R)
_ a u)
(
at level 40,
nu at level 1,
format "a *^ nu u") :
linear_ring_scope.
Notation scalable_for s f := (
mixin_of s f).
-
Notation scalable f := (
scalable_for *:%R f).
-
Notation linear_for s f := (
axiom f (
erefl s)).
-
Notation linear f := (
linear_for *:%R f).
-
Notation scalar f := (
linear_for *%R f).
+
Notation scalable f := (
scalable_for *:%R f).
+
Notation linear_for s f := (
axiom f (
erefl s)).
+
Notation linear f := (
linear_for *:%R f).
+
Notation scalar f := (
linear_for *%R f).
Notation lmorphism_for s f := (
class_of s f).
-
Notation lmorphism f := (
lmorphism_for *:%R f).
+
Notation lmorphism f := (
lmorphism_for *:%R f).
Coercion class_of_axiom : axiom >-> lmorphism_for.
Coercion base : lmorphism_for >-> Additive.axiom.
Coercion mixin : lmorphism_for >-> scalable.
Coercion apply : map >-> Funclass.
-
Notation Linear fL := (
Pack (
Phant _)
fL).
-
Notation AddLinear fZ := (
pack fZ id).
-
Notation "{ 'linear' fUV | s }" := (
map s (
Phant fUV))
+
Notation Linear fL := (
Pack (
Phant _)
fL).
+
Notation AddLinear fZ := (
pack fZ id).
+
Notation "{ 'linear' fUV | s }" := (
map s (
Phant fUV))
(
at level 0,
format "{ 'linear' fUV | s }") :
ring_scope.
-
Notation "{ 'linear' fUV }" :=
{linear fUV | *:%R}
+
Notation "{ 'linear' fUV }" :=
{linear fUV | *:%R}
(
at level 0,
format "{ 'linear' fUV }") :
ring_scope.
-
Notation "{ 'scalar' U }" :=
{linear U → _ | *%R}
+
Notation "{ 'scalar' U }" :=
{linear U → _ | *%R}
(
at level 0,
format "{ 'scalar' U }") :
ring_scope.
-
Notation "[ 'linear' 'of' f 'as' g ]" := (@
clone _ _ _ _ _ f g _ _ idfun id)
+
Notation "[ 'linear' 'of' f 'as' g ]" := (@
clone _ _ _ _ _ f g _ _ idfun id)
(
at level 0,
format "[ 'linear' 'of' f 'as' g ]") :
form_scope.
-
Notation "[ 'linear' 'of' f ]" := (@
clone _ _ _ _ _ f f _ _ id id)
+
Notation "[ 'linear' 'of' f ]" := (@
clone _ _ _ _ _ f f _ _ id id)
(
at level 0,
format "[ 'linear' 'of' f ]") :
form_scope.
Coercion additive : map >-> Additive.map.
Canonical additive.
@@ -2373,25 +2389,25 @@
Section GenericProperties.
-
Variables (
U :
lmodType R) (
V :
zmodType) (
s :
R → V → V) (
k :
unit).
-
Variable f :
{linear U → V | s}.
+
Variables (
U :
lmodType R) (
V :
zmodType) (
s :
R → V → V) (
k :
unit).
+
Variable f :
{linear U → V | s}.
-
Lemma linear0 :
f 0
= 0.
-
Lemma linearN :
{morph f : x / - x}.
-
Lemma linearD :
{morph f : x y / x + y}.
-
Lemma linearB :
{morph f : x y / x - y}.
-
Lemma linearMn n :
{morph f : x / x *+ n}.
-
Lemma linearMNn n :
{morph f : x / x *- n}.
-
Lemma linear_sum I r (
P :
pred I)
E :
-
f (
\sum_(i <- r | P i) E i)
= \sum_(i <- r | P i) f (
E i).
+
Lemma linear0 :
f 0
= 0.
+
Lemma linearN :
{morph f : x / - x}.
+
Lemma linearD :
{morph f : x y / x + y}.
+
Lemma linearB :
{morph f : x y / x - y}.
+
Lemma linearMn n :
{morph f : x / x *+ n}.
+
Lemma linearMNn n :
{morph f : x / x *- n}.
+
Lemma linear_sum I r (
P :
pred I)
E :
+
f (
\sum_(i <- r | P i) E i)
= \sum_(i <- r | P i) f (
E i).
Lemma linearZ_LR :
scalable_for s f.
-
Lemma linearP a :
{morph f : u v / a *: u + v >-> s a u + v}.
+
Lemma linearP a :
{morph f : u v / a *: u + v >-> s a u + v}.
-
Fact locked_is_scalable :
scalable_for s (
locked_with k (
f : U → V)).
+
Fact locked_is_scalable :
scalable_for s (
locked_with k (
f : U → V)).
Canonical locked_linear :=
AddLinear locked_is_scalable.
@@ -2401,7 +2417,7 @@
Section BidirectionalLinearZ.
-
Variables (
U :
lmodType R) (
V :
zmodType) (
s :
R → V → V).
+
Variables (
U :
lmodType R) (
V :
zmodType) (
s :
R → V → V).
@@ -2436,11 +2452,11 @@
-
Variables (
S :
ringType) (
h :
S → V → V) (
h_law :
Scale.law h).
+
Variables (
S :
ringType) (
h :
S → V → V) (
h_law :
Scale.law h).
Lemma linearZ c a (
h_c :=
Scale.op h_law c) (
f :
Linear.map_for U s a h_c)
u :
-
f (
a *: u)
= h_c (
Linear.wrap f u).
+
f (
a *: u)
= h_c (
Linear.wrap f u).
End BidirectionalLinearZ.
@@ -2449,18 +2465,18 @@
Section LmodProperties.
-
Variables (
U V :
lmodType R) (
f :
{linear U → V}).
+
Variables (
U V :
lmodType R) (
f :
{linear U → V}).
Lemma linearZZ :
scalable f.
Lemma linearPZ :
linear f.
-
Lemma can2_linear f' :
cancel f f' → cancel f' f → linear f'.
+
Lemma can2_linear f' :
cancel f f' → cancel f' f → linear f'.
Lemma bij_linear :
-
bijective f → exists2 f' : {linear V → U}, cancel f f' & cancel f' f.
+
bijective f → exists2 f' : {linear V → U}, cancel f f' & cancel f' f.
End LmodProperties.
@@ -2469,10 +2485,10 @@
Section ScalarProperties.
-
Variable (
U :
lmodType R) (
f :
{scalar U}).
+
Variable (
U :
lmodType R) (
f :
{scalar U}).
-
Lemma scalarZ :
scalable_for *%R f.
+
Lemma scalarZ :
scalable_for *%R f.
Lemma scalarP :
scalar f.
@@ -2482,35 +2498,35 @@
Section LinearLmod.
-
Variables (
W U :
lmodType R) (
V :
zmodType) (
s :
R → V → V).
-
Variables (
f :
{linear U → V | s}) (
h :
{linear W → U}).
+
Variables (
W U :
lmodType R) (
V :
zmodType) (
s :
R → V → V).
+
Variables (
f :
{linear U → V | s}) (
h :
{linear W → U}).
-
Lemma idfun_is_scalable :
scalable (
@idfun U).
+
Lemma idfun_is_scalable :
scalable (
@idfun U).
Canonical idfun_linear :=
AddLinear idfun_is_scalable.
-
Lemma opp_is_scalable :
scalable (
-%R : U → U).
+
Lemma opp_is_scalable :
scalable (
-%R : U → U).
Canonical opp_linear :=
AddLinear opp_is_scalable.
-
Lemma comp_is_scalable :
scalable_for s (
f \o h).
+
Lemma comp_is_scalable :
scalable_for s (
f \o h).
Canonical comp_linear :=
AddLinear comp_is_scalable.
-
Variables (
s_law :
Scale.law s) (
g :
{linear U → V | Scale.op s_law}).
-
Let Ds :
s =1 Scale.op s_law.
+
Variables (
s_law :
Scale.law s) (
g :
{linear U → V | Scale.op s_law}).
+
Let Ds :
s =1 Scale.op s_law.
-
Lemma null_fun_is_scalable :
scalable_for (
Scale.op s_law) (
\0 : U → V).
+
Lemma null_fun_is_scalable :
scalable_for (
Scale.op s_law) (
\0 : U → V).
Canonical null_fun_linear :=
AddLinear null_fun_is_scalable.
-
Lemma add_fun_is_scalable :
scalable_for s (
f \+ g).
+
Lemma add_fun_is_scalable :
scalable_for s (
f \+ g).
Canonical add_fun_linear :=
AddLinear add_fun_is_scalable.
-
Lemma sub_fun_is_scalable :
scalable_for s (
f \- g).
+
Lemma sub_fun_is_scalable :
scalable_for s (
f \- g).
Canonical sub_fun_linear :=
AddLinear sub_fun_is_scalable.
@@ -2523,10 +2539,10 @@
Variables (
A :
lalgType R) (
U :
lmodType R).
-
Variables (
a :
A) (
f :
{linear U → A}).
+
Variables (
a :
A) (
f :
{linear U → A}).
-
Fact mulr_fun_is_scalable :
scalable (
a \o× f).
+
Fact mulr_fun_is_scalable :
scalable (
a \o× f).
Canonical mulr_fun_linear :=
AddLinear mulr_fun_is_scalable.
@@ -2542,30 +2558,30 @@
Section ClassDef.
-
Variables (
R :
ringType) (
A :
lalgType R) (
B :
ringType) (
s :
R → B → B).
+
Variables (
R :
ringType) (
A :
lalgType R) (
B :
ringType) (
s :
R → B → B).
-
Record class_of (
f :
A → B) :
Prop :=
+
Record class_of (
f :
A → B) :
Prop :=
Class {
base :
rmorphism f;
mixin :
scalable_for s f}.
Definition base2 f (
fLM :
class_of f) :=
Linear.Class fLM (
mixin fLM).
-
Structure map (
phAB :
phant (
A → B)) :=
Pack {
apply;
_ :
class_of apply}.
+
Structure map (
phAB :
phant (
A → B)) :=
Pack {
apply;
_ :
class_of apply}.
-
Variables (
phAB :
phant (
A → B)) (
f :
A → B) (
cF :
map phAB).
+
Variables (
phAB :
phant (
A → B)) (
f :
A → B) (
cF :
map phAB).
Definition class :=
let:
Pack _ c as cF' :=
cF return class_of cF' in c.
Definition clone :=
-
fun (
g :
RMorphism.map phAB)
fM &
phant_id (
RMorphism.class g)
fM ⇒
+
fun (
g :
RMorphism.map phAB)
fM &
phant_id (
RMorphism.class g)
fM ⇒
fun (
h :
Linear.map s phAB)
fZ &
-
phant_id (
Linear.mixin (
Linear.class h))
fZ ⇒
+
phant_id (
Linear.mixin (
Linear.class h))
fZ ⇒
Pack phAB (@
Class f fM fZ).
Definition pack (
fZ :
scalable_for s f) :=
-
fun (
g :
RMorphism.map phAB)
fM &
phant_id (
RMorphism.class g)
fM ⇒
+
fun (
g :
RMorphism.map phAB)
fM &
phant_id (
RMorphism.class g)
fM ⇒
Pack phAB (
Class fM fZ).
@@ -2581,17 +2597,17 @@
Module Exports.
Notation lrmorphism_for s f := (
class_of s f).
-
Notation lrmorphism f := (
lrmorphism_for *:%R f).
+
Notation lrmorphism f := (
lrmorphism_for *:%R f).
Coercion base : lrmorphism_for >-> RMorphism.class_of.
Coercion base2 : lrmorphism_for >-> lmorphism_for.
Coercion apply : map >-> Funclass.
-
Notation LRMorphism f_lrM := (
Pack (
Phant _) (
Class f_lrM f_lrM)).
-
Notation AddLRMorphism fZ := (
pack fZ id).
-
Notation "{ 'lrmorphism' fAB | s }" := (
map s (
Phant fAB))
+
Notation LRMorphism f_lrM := (
Pack (
Phant _) (
Class f_lrM f_lrM)).
+
Notation AddLRMorphism fZ := (
pack fZ id).
+
Notation "{ 'lrmorphism' fAB | s }" := (
map s (
Phant fAB))
(
at level 0,
format "{ 'lrmorphism' fAB | s }") :
ring_scope.
-
Notation "{ 'lrmorphism' fAB }" :=
{lrmorphism fAB | *:%R}
+
Notation "{ 'lrmorphism' fAB }" :=
{lrmorphism fAB | *:%R}
(
at level 0,
format "{ 'lrmorphism' fAB }") :
ring_scope.
-
Notation "[ 'lrmorphism' 'of' f ]" := (@
clone _ _ _ _ _ f _ _ id _ _ id)
+
Notation "[ 'lrmorphism' 'of' f ]" := (@
clone _ _ _ _ _ f _ _ id _ _ id)
(
at level 0,
format "[ 'lrmorphism' 'of' f ]") :
form_scope.
Coercion additive : map >-> Additive.map.
Canonical additive.
@@ -2611,26 +2627,26 @@
Section LRMorphismTheory.
-
Variables (
R :
ringType) (
A B :
lalgType R) (
C :
ringType) (
s :
R → C → C).
-
Variables (
k :
unit) (
f :
{lrmorphism A → B}) (
g :
{lrmorphism B → C | s}).
+
Variables (
R :
ringType) (
A B :
lalgType R) (
C :
ringType) (
s :
R → C → C).
+
Variables (
k :
unit) (
f :
{lrmorphism A → B}) (
g :
{lrmorphism B → C | s}).
-
Definition idfun_lrmorphism :=
[lrmorphism of @idfun A].
-
Definition comp_lrmorphism :=
[lrmorphism of g \o f].
-
Definition locked_lrmorphism :=
[lrmorphism of locked_with k (
f : A → B)
].
+
Definition idfun_lrmorphism :=
[lrmorphism of @idfun A].
+
Definition comp_lrmorphism :=
[lrmorphism of g \o f].
+
Definition locked_lrmorphism :=
[lrmorphism of locked_with k (
f : A → B)
].
-
Lemma rmorph_alg a :
f a%:A = a%:A.
+
Lemma rmorph_alg a :
f a%:A = a%:A.
Lemma lrmorphismP :
lrmorphism f.
-
Lemma can2_lrmorphism f' :
cancel f f' → cancel f' f → lrmorphism f'.
+
Lemma can2_lrmorphism f' :
cancel f f' → cancel f' f → lrmorphism f'.
Lemma bij_lrmorphism :
-
bijective f → exists2 f' : {lrmorphism B → A}, cancel f f' & cancel f' f.
+
bijective f → exists2 f' : {lrmorphism B → A}, cancel f f' & cancel f' f.
End LRMorphismTheory.
@@ -2649,26 +2665,26 @@
Record class_of R :=
-
Class {
base :
Ring.class_of R;
mixin :
commutative (
Ring.mul base)}.
+
Class {
base :
Ring.class_of R;
mixin :
commutative (
Ring.mul base)}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variable (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack mul0 (
m0 : @
commutative T T mul0) :=
-
fun bT b &
phant_id (
Ring.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
Definition pack mul0 (
m0 : @
commutative T T mul0) :=
+
fun bT b &
phant_id (
Ring.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
End ClassDef.
@@ -2687,11 +2703,11 @@
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Notation comRingType :=
type.
-
Notation ComRingType T m := (@
pack T _ m _ _ id _ id).
+
Notation ComRingType T m := (@
pack T _ m _ _ id _ id).
Notation ComRingMixin :=
RingMixin.
-
Notation "[ 'comRingType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation "[ 'comRingType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'comRingType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'comRingType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'comRingType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'comRingType' 'of' T ]") :
form_scope.
End Exports.
@@ -2707,53 +2723,53 @@
Implicit Types x y :
R.
-
Lemma mulrC : @
commutative R R *%R.
+
Lemma mulrC : @
commutative R R *%R.
Canonical mul_comoid :=
Monoid.ComLaw mulrC.
-
Lemma mulrCA : @
left_commutative R R *%R.
-
Lemma mulrAC : @
right_commutative R R *%R.
-
Lemma mulrACA : @
interchange R *%R *%R.
+
Lemma mulrCA : @
left_commutative R R *%R.
+
Lemma mulrAC : @
right_commutative R R *%R.
+
Lemma mulrACA : @
interchange R *%R *%R.
-
Lemma exprMn n :
{morph (fun x ⇒
x ^+ n) : x y / x × y}.
+
Lemma exprMn n :
{morph (fun x ⇒
x ^+ n) : x y / x × y}.
-
Lemma prodrXl n I r (
P :
pred I) (
F :
I → R) :
-
\prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n.
+
Lemma prodrXl n I r (
P :
pred I) (
F :
I → R) :
+
\prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n.
-
Lemma prodr_undup_exp_count (
I :
eqType)
r (
P :
pred I) (
F :
I → R) :
-
\prod_(i <- undup r | P i) F i ^+ count_mem i r = \prod_(i <- r | P i) F i.
+
Lemma prodr_undup_exp_count (
I :
eqType)
r (
P :
pred I) (
F :
I → R) :
+
\prod_(i <- undup r | P i) F i ^+ count_mem i r = \prod_(i <- r | P i) F i.
Lemma exprDn x y n :
-
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
+
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma exprBn x y n :
-
(x - y) ^+ n =
-
\sum_(i < n.+1) ((-1
) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
+
(x - y) ^+ n =
+
\sum_(i < n.+1) ((-1
) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma subrXX x y n :
-
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
+
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
-
Lemma sqrrD x y :
(x + y) ^+ 2
= x ^+ 2
+ x × y *+ 2
+ y ^+ 2.
+
Lemma sqrrD x y :
(x + y) ^+ 2
= x ^+ 2
+ x × y *+ 2
+ y ^+ 2.
-
Lemma sqrrB x y :
(x - y) ^+ 2
= x ^+ 2
- x × y *+ 2
+ y ^+ 2.
+
Lemma sqrrB x y :
(x - y) ^+ 2
= x ^+ 2
- x × y *+ 2
+ y ^+ 2.
-
Lemma subr_sqr x y :
x ^+ 2
- y ^+ 2
= (x - y) × (x + y).
+
Lemma subr_sqr x y :
x ^+ 2
- y ^+ 2
= (x - y) × (x + y).
-
Lemma subr_sqrDB x y :
(x + y) ^+ 2
- (x - y) ^+ 2
= x × y *+ 4.
+
Lemma subr_sqrDB x y :
(x + y) ^+ 2
- (x - y) ^+ 2
= x × y *+ 4.
Section FrobeniusAutomorphism.
-
Variables (
p :
nat) (
charRp :
p \in [char R]).
+
Variables (
p :
nat) (
charRp :
p \in [char R]).
Lemma Frobenius_aut_is_rmorphism :
rmorphism (
Frobenius_aut charRp).
@@ -2766,24 +2782,24 @@
End FrobeniusAutomorphism.
-
Lemma exprDn_char x y n :
[char R].-nat n → (x + y) ^+ n = x ^+ n + y ^+ n.
+
Lemma exprDn_char x y n :
[char R].-nat n → (x + y) ^+ n = x ^+ n + y ^+ n.
-
Lemma rmorph_comm (
S :
ringType) (
f :
{rmorphism R → S})
x y :
+
Lemma rmorph_comm (
S :
ringType) (
f :
{rmorphism R → S})
x y :
comm (
f x) (
f y).
Section ScaleLinear.
-
Variables (
U V :
lmodType R) (
b :
R) (
f :
{linear U → V}).
+
Variables (
U V :
lmodType R) (
b :
R) (
f :
{linear U → V}).
-
Lemma scale_is_scalable :
scalable (
*:%R b : V → V).
+
Lemma scale_is_scalable :
scalable (
*:%R b : V → V).
Canonical scale_linear :=
AddLinear scale_is_scalable.
-
Lemma scale_fun_is_scalable :
scalable (
b \*: f).
+
Lemma scale_fun_is_scalable :
scalable (
b \*: f).
Canonical scale_fun_linear :=
AddLinear scale_fun_is_scalable.
@@ -2802,10 +2818,10 @@
Variables (
R :
ringType) (
A :
lalgType R).
-
Definition axiom :=
∀ k (
x y :
A),
k *: (x × y) = x × (k *: y).
+
Definition axiom :=
∀ k (
x y :
A),
k *: (x × y) = x × (k *: y).
-
Lemma comm_axiom :
phant A → commutative (@
mul A)
→ axiom.
+
Lemma comm_axiom :
phant A → commutative (@
mul A)
→ axiom.
End Mixin.
@@ -2819,29 +2835,29 @@
Record class_of (
T :
Type) :
Type :=
Class {
base :
Lalgebra.class_of R T;
-
mixin :
axiom (
Lalgebra.Pack _ base T)
+
mixin :
axiom (
Lalgebra.Pack _ base)
}.
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack phR T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack phR T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
Definition pack b0 (
ax0 : @
axiom R b0) :=
-
fun bT b &
phant_id (@
Lalgebra.class R phR bT)
b ⇒
-
fun ax &
phant_id ax0 ax ⇒
Pack phR (@
Class T b ax)
T.
+
fun bT b &
phant_id (@
Lalgebra.class R phR bT)
b ⇒
+
fun ax &
phant_id ax0 ax ⇒
Pack phR (@
Class T b ax).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition lmodType := @
Lmodule.Pack R phR cT xclass xT.
-
Definition lalgType := @
Lalgebra.Pack R phR cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition lmodType := @
Lmodule.Pack R phR cT xclass.
+
Definition lalgType := @
Lalgebra.Pack R phR cT xclass.
End ClassDef.
@@ -2862,13 +2878,13 @@
Canonical lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical lalgType.
-
Notation algType R := (
type (
Phant R)).
-
Notation AlgType R A ax := (@
pack _ (
Phant R)
A _ ax _ _ id _ id).
-
Notation CommAlgType R A := (
AlgType R A (
comm_axiom (
Phant A) (@
mulrC _))).
-
Notation "[ 'algType' R 'of' T 'for' cT ]" := (@
clone _ (
Phant R)
T cT _ idfun)
+
Notation algType R := (
type (
Phant R)).
+
Notation AlgType R A ax := (@
pack _ (
Phant R)
A _ ax _ _ id _ id).
+
Notation CommAlgType R A := (
AlgType R A (
comm_axiom (
Phant A) (@
mulrC _))).
+
Notation "[ 'algType' R 'of' T 'for' cT ]" := (@
clone _ (
Phant R)
T cT _ idfun)
(
at level 0,
format "[ 'algType' R 'of' T 'for' cT ]")
:
form_scope.
-
Notation "[ 'algType' R 'of' T ]" := (@
clone _ (
Phant R)
T _ _ id)
+
Notation "[ 'algType' R 'of' T ]" := (@
clone _ (
Phant R)
T _ _ id)
(
at level 0,
format "[ 'algType' R 'of' T ]") :
form_scope.
End Exports.
@@ -2884,39 +2900,39 @@
Implicit Types (
k :
R) (
x y :
A).
-
Lemma scalerAr k x y :
k *: (x × y) = x × (k *: y).
+
Lemma scalerAr k x y :
k *: (x × y) = x × (k *: y).
-
Lemma scalerCA k x y :
k *: x × y = x × (k *: y).
+
Lemma scalerCA k x y :
k *: x × y = x × (k *: y).
-
Lemma mulr_algr a x :
x × a%:A = a *: x.
+
Lemma mulr_algr a x :
x × a%:A = a *: x.
-
Lemma exprZn k x n :
(k *: x) ^+ n = k ^+ n *: x ^+ n.
+
Lemma exprZn k x n :
(k *: x) ^+ n = k ^+ n *: x ^+ n.
-
Lemma scaler_prod I r (
P :
pred I) (
F :
I → R) (
G :
I → A) :
-
\prod_(i <- r | P i) (F i *: G i) =
-
\prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.
+
Lemma scaler_prod I r (
P :
pred I) (
F :
I → R) (
G :
I → A) :
+
\prod_(i <- r | P i) (F i *: G i) =
+
\prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.
-
Lemma scaler_prodl (
I :
finType) (
S :
pred I) (
F :
I → A)
k :
-
\prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.
+
Lemma scaler_prodl (
I :
finType) (
S :
pred I) (
F :
I → A)
k :
+
\prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.
-
Lemma scaler_prodr (
I :
finType) (
S :
pred I) (
F :
I → R)
x :
-
\prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.
+
Lemma scaler_prodr (
I :
finType) (
S :
pred I) (
F :
I → R)
x :
+
\prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.
-
Canonical regular_comRingType :=
[comRingType of R^o].
-
Canonical regular_algType :=
CommAlgType R R^o.
+
Canonical regular_comRingType :=
[comRingType of R^o].
+
Canonical regular_algType :=
CommAlgType R R^o.
-
Variables (
U :
lmodType R) (
a :
A) (
f :
{linear U → A}).
+
Variables (
U :
lmodType R) (
a :
A) (
f :
{linear U → A}).
-
Lemma mull_fun_is_scalable :
scalable (
a \*o f).
+
Lemma mull_fun_is_scalable :
scalable (
a \*o f).
Canonical mull_fun_linear :=
AddLinear mull_fun_is_scalable.
@@ -2927,18 +2943,18 @@
Record mixin_of (
R :
ringType) :
Type :=
Mixin {
-
unit :
pred R;
-
inv :
R → R;
-
_ :
{in unit, left_inverse 1
inv *%R};
-
_ :
{in unit, right_inverse 1
inv *%R};
-
_ :
∀ x y,
y × x = 1
∧ x × y = 1
→ unit x;
-
_ :
{in [predC unit], inv =1 id}
+
unit :
pred R;
+
inv :
R → R;
+
_ :
{in unit, left_inverse 1
inv *%R};
+
_ :
{in unit, right_inverse 1
inv *%R};
+
_ :
∀ x y,
y × x = 1
∧ x × y = 1
→ unit x;
+
_ :
{in [predC unit], inv =1 id}
}.
Definition EtaMixin R unit inv mulVr mulrV unitP inv_out :=
let _ := @
Mixin R unit inv mulVr mulrV unitP inv_out in
- @
Mixin (
Ring.Pack (
Ring.class R)
R)
unit inv mulVr mulrV unitP inv_out.
+ @
Mixin (
Ring.Pack (
Ring.class R))
unit inv mulVr mulrV unitP inv_out.
Section ClassDef.
@@ -2946,27 +2962,27 @@
Record class_of (
R :
Type) :
Type :=
Class {
base :
Ring.class_of R;
-
mixin :
mixin_of (
Ring.Pack base R)
+
mixin :
mixin_of (
Ring.Pack base)
}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack b0 (
m0 :
mixin_of (@
Ring.Pack T b0 T)) :=
-
fun bT b &
phant_id (
Ring.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
Definition pack b0 (
m0 :
mixin_of (@
Ring.Pack T b0)) :=
+
fun bT b &
phant_id (
Ring.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
End ClassDef.
@@ -2985,11 +3001,11 @@
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Notation unitRingType :=
type.
-
Notation UnitRingType T m := (@
pack T _ m _ _ id _ id).
+
Notation UnitRingType T m := (@
pack T _ m _ _ id _ id).
Notation UnitRingMixin :=
EtaMixin.
-
Notation "[ 'unitRingType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation "[ 'unitRingType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'unitRingType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'unitRingType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'unitRingType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'unitRingType' 'of' T ]") :
form_scope.
End Exports.
@@ -2999,10 +3015,10 @@
Definition unit {
R :
unitRingType} :=
-
[qualify a u : R | UnitRing.unit (
UnitRing.class R)
u].
-
Fact unit_key R :
pred_key (@
unit R).
-
Canonical unit_keyed R :=
KeyedQualifier (@
unit_key R).
-
Definition inv {
R :
unitRingType} :
R → R :=
UnitRing.inv (
UnitRing.class R).
+
[qualify a u : R | UnitRing.unit (
UnitRing.class R)
u].
+
Fact unit_key R :
pred_key (@
unit R).
+
Canonical unit_keyed R :=
KeyedQualifier (@
unit_key R).
+
Definition inv {
R :
unitRingType} :
R → R :=
UnitRing.inv (
UnitRing.class R).
@@ -3014,36 +3030,36 @@
Implicit Types x y :
R.
-
Lemma divrr :
{in unit, right_inverse 1 (@
inv R)
*%R}.
+
Lemma divrr :
{in unit, right_inverse 1 (@
inv R)
*%R}.
Definition mulrV :=
divrr.
-
Lemma mulVr :
{in unit, left_inverse 1 (@
inv R)
*%R}.
+
Lemma mulVr :
{in unit, left_inverse 1 (@
inv R)
*%R}.
-
Lemma invr_out x :
x \isn't a unit → x^-1 = x.
+
Lemma invr_out x :
x \isn't a unit → x^-1 = x.
-
Lemma unitrP x :
reflect (
∃ y, y × x = 1
∧ x × y = 1) (
x \is a unit).
+
Lemma unitrP x :
reflect (
∃ y, y × x = 1
∧ x × y = 1) (
x \is a unit).
-
Lemma mulKr :
{in unit, left_loop (@
inv R)
*%R}.
+
Lemma mulKr :
{in unit, left_loop (@
inv R)
*%R}.
-
Lemma mulVKr :
{in unit, rev_left_loop (@
inv R)
*%R}.
+
Lemma mulVKr :
{in unit, rev_left_loop (@
inv R)
*%R}.
-
Lemma mulrK :
{in unit, right_loop (@
inv R)
*%R}.
+
Lemma mulrK :
{in unit, right_loop (@
inv R)
*%R}.
-
Lemma mulrVK :
{in unit, rev_right_loop (@
inv R)
*%R}.
+
Lemma mulrVK :
{in unit, rev_right_loop (@
inv R)
*%R}.
Definition divrK :=
mulrVK.
-
Lemma mulrI :
{in @
unit R, right_injective *%R}.
+
Lemma mulrI :
{in @
unit R, right_injective *%R}.
-
Lemma mulIr :
{in @
unit R, left_injective *%R}.
+
Lemma mulIr :
{in @
unit R, left_injective *%R}.
@@ -3052,134 +3068,133 @@
Due to noncommutativity, fractions are inverted.
-
Lemma telescope_prodr n m (
f :
nat → R) :
-
(∀ k,
n < k < m → f k \is a unit) → n < m →
-
\prod_(n ≤ k < m) (f k / f k.+1) = f n / f m.
+
Lemma telescope_prodr n m (
f :
nat → R) :
+
(∀ k,
n < k < m → f k \is a unit) → n < m →
+
\prod_(n ≤ k < m) (f k / f k.+1) = f n / f m.
-
Lemma commrV x y :
comm x y → comm x y^-1.
+
Lemma commrV x y :
comm x y → comm x y^-1.
-
Lemma unitrE x :
(x \is a unit) = (x / x == 1
).
+
Lemma unitrE x :
(x \is a unit) = (x / x == 1
).
-
Lemma invrK :
involutive (@
inv R).
+
Lemma invrK :
involutive (@
inv R).
-
Lemma invr_inj :
injective (@
inv R).
+
Lemma invr_inj :
injective (@
inv R).
-
Lemma unitrV x :
(x^-1 \in unit) = (x \in unit).
+
Lemma unitrV x :
(x^-1 \in unit) = (x \in unit).
-
Lemma unitr1 : 1
\in @
unit R.
+
Lemma unitr1 : 1
\in @
unit R.
-
Lemma invr1 : 1
^-1 = 1
:> R.
+
Lemma invr1 : 1
^-1 = 1
:> R.
-
Lemma div1r x : 1
/ x = x^-1.
-
Lemma divr1 x :
x / 1
= x.
+
Lemma div1r x : 1
/ x = x^-1.
+
Lemma divr1 x :
x / 1
= x.
Lemma natr_div m d :
-
d %| m → d%:R \is a @
unit R → (m %/ d)%:R = m%:R / d%:R :> R.
+
d %| m → d%:R \is a @
unit R → (m %/ d)%:R = m%:R / d%:R :> R.
-
Lemma divrI :
{in unit, right_injective (
fun x y ⇒
x / y)
}.
+
Lemma divrI :
{in unit, right_injective (
fun x y ⇒
x / y)
}.
-
Lemma divIr :
{in unit, left_injective (
fun x y ⇒
x / y)
}.
+
Lemma divIr :
{in unit, left_injective (
fun x y ⇒
x / y)
}.
-
Lemma unitr0 :
(0
\is a @
unit R) = false.
+
Lemma unitr0 :
(0
\is a @
unit R) = false.
-
Lemma invr0 : 0
^-1 = 0
:> R.
+
Lemma invr0 : 0
^-1 = 0
:> R.
-
Lemma unitrN1 : -1
\is a @
unit R.
+
Lemma unitrN1 : -1
\is a @
unit R.
-
Lemma invrN1 :
(-1
)^-1 = -1
:> R.
+
Lemma invrN1 :
(-1
)^-1 = -1
:> R.
-
Lemma invr_sign n :
((-1
) ^- n) = (-1
) ^+ n :> R.
+
Lemma invr_sign n :
((-1
) ^- n) = (-1
) ^+ n :> R.
-
Lemma unitrMl x y :
y \is a unit → (x × y \is a unit) = (x \is a unit).
+
Lemma unitrMl x y :
y \is a unit → (x × y \is a unit) = (x \is a unit).
-
Lemma unitrMr x y :
x \is a unit → (x × y \is a unit) = (y \is a unit).
+
Lemma unitrMr x y :
x \is a unit → (x × y \is a unit) = (y \is a unit).
-
Lemma invrM :
{in unit &, ∀ x y,
(x × y)^-1 = y^-1 × x^-1}.
+
Lemma invrM :
{in unit &, ∀ x y,
(x × y)^-1 = y^-1 × x^-1}.
Lemma unitrM_comm x y :
-
comm x y → (x × y \is a unit) = (x \is a unit) && (y \is a unit).
+
comm x y → (x × y \is a unit) = (x \is a unit) && (y \is a unit).
-
Lemma unitrX x n :
x \is a unit → x ^+ n \is a unit.
+
Lemma unitrX x n :
x \is a unit → x ^+ n \is a unit.
-
Lemma unitrX_pos x n :
n > 0
→ (x ^+ n \in unit) = (x \in unit).
+
Lemma unitrX_pos x n :
n > 0
→ (x ^+ n \in unit) = (x \in unit).
-
Lemma exprVn x n :
x^-1 ^+ n = x ^- n.
+
Lemma exprVn x n :
x^-1 ^+ n = x ^- n.
-
Lemma exprB m n x :
n ≤ m → x \is a unit → x ^+ (m - n) = x ^+ m / x ^+ n.
+
Lemma exprB m n x :
n ≤ m → x \is a unit → x ^+ (m - n) = x ^+ m / x ^+ n.
-
Lemma invr_neq0 x :
x != 0
→ x^-1 != 0.
+
Lemma invr_neq0 x :
x != 0
→ x^-1 != 0.
-
Lemma invr_eq0 x :
(x^-1 == 0
) = (x == 0
).
+
Lemma invr_eq0 x :
(x^-1 == 0
) = (x == 0
).
-
Lemma invr_eq1 x :
(x^-1 == 1
) = (x == 1
).
+
Lemma invr_eq1 x :
(x^-1 == 1
) = (x == 1
).
-
Lemma rev_unitrP (
x y :
R^c) :
y × x = 1
∧ x × y = 1
→ x \is a unit.
+
Lemma rev_unitrP (
x y :
R^c) :
y × x = 1
∧ x × y = 1
→ x \is a unit.
Definition converse_unitRingMixin :=
- @
UnitRing.Mixin _ (
(unit : pred_class) : pred R^c)
_
-
mulrV mulVr rev_unitrP invr_out.
-
Canonical converse_unitRingType :=
UnitRingType R^c converse_unitRingMixin.
-
Canonical regular_unitRingType :=
[unitRingType of R^o].
+ @
UnitRing.Mixin _ (
unit : {pred R^c})
_ mulrV mulVr rev_unitrP invr_out.
+
Canonical converse_unitRingType :=
UnitRingType R^c converse_unitRingMixin.
+
Canonical regular_unitRingType :=
[unitRingType of R^o].
Section ClosedPredicates.
-
Variables S :
predPredType R.
+
Variables S :
{pred R}.
-
Definition invr_closed :=
{in S, ∀ x,
x^-1 \in S}.
-
Definition divr_2closed :=
{in S &, ∀ x y,
x / y \in S}.
-
Definition divr_closed := 1
\in S ∧ divr_2closed.
-
Definition sdivr_closed := -1
\in S ∧ divr_2closed.
-
Definition divring_closed :=
[/\ 1
\in S, subr_2closed S & divr_2closed].
+
Definition invr_closed :=
{in S, ∀ x,
x^-1 \in S}.
+
Definition divr_2closed :=
{in S &, ∀ x y,
x / y \in S}.
+
Definition divr_closed := 1
\in S ∧ divr_2closed.
+
Definition sdivr_closed := -1
\in S ∧ divr_2closed.
+
Definition divring_closed :=
[/\ 1
\in S, subr_2closed S & divr_2closed].
-
Lemma divr_closedV :
divr_closed → invr_closed.
+
Lemma divr_closedV :
divr_closed → invr_closed.
-
Lemma divr_closedM :
divr_closed → mulr_closed S.
+
Lemma divr_closedM :
divr_closed → mulr_closed S.
-
Lemma sdivr_closed_div :
sdivr_closed → divr_closed.
+
Lemma sdivr_closed_div :
sdivr_closed → divr_closed.
-
Lemma sdivr_closedM :
sdivr_closed → smulr_closed S.
+
Lemma sdivr_closedM :
sdivr_closed → smulr_closed S.
-
Lemma divring_closedBM :
divring_closed → subring_closed S.
+
Lemma divring_closedBM :
divring_closed → subring_closed S.
-
Lemma divring_closed_div :
divring_closed → sdivr_closed.
+
Lemma divring_closed_div :
divring_closed → sdivr_closed.
End ClosedPredicates.
@@ -3193,16 +3208,16 @@
Section UnitRingMorphism.
-
Variables (
R S :
unitRingType) (
f :
{rmorphism R → S}).
+
Variables (
R S :
unitRingType) (
f :
{rmorphism R → S}).
-
Lemma rmorph_unit x :
x \in unit → f x \in unit.
+
Lemma rmorph_unit x :
x \in unit → f x \in unit.
-
Lemma rmorphV :
{in unit, {morph f: x / x^-1}}.
+
Lemma rmorphV :
{in unit, {morph f: x / x^-1}}.
-
Lemma rmorph_div x y :
y \in unit → f (
x / y)
= f x / f y.
+
Lemma rmorph_div x y :
y \in unit → f (
x / y)
= f x / f y.
End UnitRingMorphism.
@@ -3214,15 +3229,15 @@
Section Mixin.
-
Variables (
R :
comRingType) (
unit :
pred R) (
inv :
R → R).
-
Hypothesis mulVx :
{in unit, left_inverse 1
inv *%R}.
-
Hypothesis unitPl :
∀ x y,
y × x = 1
→ unit x.
+
Variables (
R :
comRingType) (
unit :
pred R) (
inv :
R → R).
+
Hypothesis mulVx :
{in unit, left_inverse 1
inv *%R}.
+
Hypothesis unitPl :
∀ x y,
y × x = 1
→ unit x.
-
Fact mulC_mulrV :
{in unit, right_inverse 1
inv *%R}.
+
Fact mulC_mulrV :
{in unit, right_inverse 1
inv *%R}.
-
Fact mulC_unitP x y :
y × x = 1
∧ x × y = 1
→ unit x.
+
Fact mulC_unitP x y :
y × x = 1
∧ x × y = 1
→ unit x.
Definition Mixin :=
UnitRingMixin mulVx mulC_mulrV mulC_unitP.
@@ -3236,31 +3251,31 @@
Record class_of (
R :
Type) :
Type :=
Class {
base :
ComRing.class_of R;
-
mixin :
UnitRing.mixin_of (
Ring.Pack base R)
+
mixin :
UnitRing.mixin_of (
Ring.Pack base)
}.
Definition base2 R m :=
UnitRing.Class (@
mixin R m).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
Definition pack :=
-
fun bT b &
phant_id (
ComRing.class bT) (
b : ComRing.class_of T) ⇒
-
fun mT m &
phant_id (
UnitRing.class mT) (@
UnitRing.Class T b m) ⇒
-
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
ComRing.class bT) (
b : ComRing.class_of T) ⇒
+
fun mT m &
phant_id (
UnitRing.class mT) (@
UnitRing.Class T b m) ⇒
+
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition com_unitRingType := @
UnitRing.Pack comRingType xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
UnitRing.Pack cT xclass.
+
Definition com_unitRingType := @
UnitRing.Pack comRingType xclass.
End ClassDef.
@@ -3286,7 +3301,7 @@
Canonical com_unitRingType.
Notation comUnitRingType :=
type.
Notation ComUnitRingMixin :=
Mixin.
-
Notation "[ 'comUnitRingType' 'of' T ]" := (@
pack T _ _ id _ _ id)
+
Notation "[ 'comUnitRingType' 'of' T ]" := (@
pack T _ _ id _ _ id)
(
at level 0,
format "[ 'comUnitRingType' 'of' T ]") :
form_scope.
End Exports.
@@ -3306,35 +3321,35 @@
Record class_of (
T :
Type) :
Type :=
Class {
base :
Algebra.class_of R T;
-
mixin :
GRing.UnitRing.mixin_of (
Ring.Pack base T)
+
mixin :
GRing.UnitRing.mixin_of (
Ring.Pack base)
}.
Definition base2 R m :=
UnitRing.Class (@
mixin R m).
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variable (
phR :
phant R) (
T :
Type) (
cT :
type phR).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
Definition pack :=
-
fun bT b &
phant_id (@
Algebra.class R phR bT) (
b : Algebra.class_of R T) ⇒
-
fun mT m &
phant_id (
UnitRing.mixin (
UnitRing.class mT))
m ⇒
-
Pack (
Phant R) (@
Class T b m)
T.
+
fun bT b &
phant_id (@
Algebra.class R phR bT) (
b : Algebra.class_of R T) ⇒
+
fun mT m &
phant_id (
UnitRing.mixin (
UnitRing.class mT))
m ⇒
+
Pack (
Phant R) (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition unitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition lmodType := @
Lmodule.Pack R phR cT xclass xT.
-
Definition lalgType := @
Lalgebra.Pack R phR cT xclass xT.
-
Definition algType := @
Algebra.Pack R phR cT xclass xT.
-
Definition lmod_unitRingType := @
Lmodule.Pack R phR unitRingType xclass xT.
-
Definition lalg_unitRingType := @
Lalgebra.Pack R phR unitRingType xclass xT.
-
Definition alg_unitRingType := @
Algebra.Pack R phR unitRingType xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition unitRingType := @
UnitRing.Pack cT xclass.
+
Definition lmodType := @
Lmodule.Pack R phR cT xclass.
+
Definition lalgType := @
Lalgebra.Pack R phR cT xclass.
+
Definition algType := @
Algebra.Pack R phR cT xclass.
+
Definition lmod_unitRingType := @
Lmodule.Pack R phR unitRingType xclass.
+
Definition lalg_unitRingType := @
Lalgebra.Pack R phR unitRingType xclass.
+
Definition alg_unitRingType := @
Algebra.Pack R phR unitRingType xclass.
End ClassDef.
@@ -3363,8 +3378,8 @@
Canonical lmod_unitRingType.
Canonical lalg_unitRingType.
Canonical alg_unitRingType.
-
Notation unitAlgType R := (
type (
Phant R)).
-
Notation "[ 'unitAlgType' R 'of' T ]" := (@
pack _ (
Phant R)
T _ _ id _ _ id)
+
Notation unitAlgType R := (
type (
Phant R)).
+
Notation "[ 'unitAlgType' R 'of' T ]" := (@
pack _ (
Phant R)
T _ _ id _ _ id)
(
at level 0,
format "[ 'unitAlgType' R 'of' T ]") :
form_scope.
End Exports.
@@ -3380,26 +3395,26 @@
Implicit Types x y :
R.
-
Lemma unitrM x y :
(x × y \in unit) = (x \in unit) && (y \in unit).
+
Lemma unitrM x y :
(x × y \in unit) = (x \in unit) && (y \in unit).
-
Lemma unitrPr x :
reflect (
∃ y, x × y = 1) (
x \in unit).
+
Lemma unitrPr x :
reflect (
∃ y, x × y = 1) (
x \in unit).
-
Lemma mulr1_eq x y :
x × y = 1
→ x^-1 = y.
+
Lemma mulr1_eq x y :
x × y = 1
→ x^-1 = y.
-
Lemma divr1_eq x y :
x / y = 1
→ x = y.
+
Lemma divr1_eq x y :
x / y = 1
→ x = y.
-
Lemma divKr x :
x \is a unit → {in unit, involutive (
fun y ⇒
x / y)
}.
+
Lemma divKr x :
x \is a unit → {in unit, involutive (
fun y ⇒
x / y)
}.
-
Lemma expr_div_n x y n :
(x / y) ^+ n = x ^+ n / y ^+ n.
+
Lemma expr_div_n x y n :
(x / y) ^+ n = x ^+ n / y ^+ n.
-
Canonical regular_comUnitRingType :=
[comUnitRingType of R^o].
-
Canonical regular_unitAlgType :=
[unitAlgType R of R^o].
+
Canonical regular_comUnitRingType :=
[comUnitRingType of R^o].
+
Canonical regular_unitAlgType :=
[unitAlgType R of R^o].
End ComUnitRingTheory.
@@ -3412,28 +3427,28 @@
Implicit Types (
k :
R) (
x y :
A).
-
Lemma scaler_injl :
{in unit, @
right_injective R A A *:%R}.
+
Lemma scaler_injl :
{in unit, @
right_injective R A A *:%R}.
-
Lemma scaler_unit k x :
k \in unit → (k *: x \in unit) = (x \in unit).
+
Lemma scaler_unit k x :
k \in unit → (k *: x \in unit) = (x \in unit).
-
Lemma invrZ k x :
k \in unit → x \in unit → (k *: x)^-1 = k^-1 *: x^-1.
+
Lemma invrZ k x :
k \in unit → x \in unit → (k *: x)^-1 = k^-1 *: x^-1.
Section ClosedPredicates.
-
Variables S :
predPredType A.
+
Variables S :
{pred A}.
-
Definition divalg_closed :=
[/\ 1
\in S, linear_closed S & divr_2closed S].
+
Definition divalg_closed :=
[/\ 1
\in S, linear_closed S & divr_2closed S].
-
Lemma divalg_closedBdiv :
divalg_closed → divring_closed S.
+
Lemma divalg_closedBdiv :
divalg_closed → divring_closed S.
-
Lemma divalg_closedZ :
divalg_closed → subalg_closed S.
+
Lemma divalg_closedZ :
divalg_closed → subalg_closed S.
End ClosedPredicates.
@@ -3451,9 +3466,9 @@
Module Pred.
-
Structure opp V S :=
Opp {
opp_key :
pred_key S;
_ : @
oppr_closed V S}.
-
Structure add V S :=
Add {
add_key :
pred_key S;
_ : @
addr_closed V S}.
-
Structure mul R S :=
Mul {
mul_key :
pred_key S;
_ : @
mulr_closed R S}.
+
Structure opp V S :=
Opp {
opp_key :
pred_key S;
_ : @
oppr_closed V S}.
+
Structure add V S :=
Add {
add_key :
pred_key S;
_ : @
addr_closed V S}.
+
Structure mul R S :=
Mul {
mul_key :
pred_key S;
_ : @
mulr_closed R S}.
Structure zmod V S :=
Zmod {
zmod_add :
add S;
_ : @
oppr_closed V S}.
Structure semiring R S :=
Semiring {
semiring_add :
add S;
_ : @
mulr_closed R S}.
Structure smul R S :=
Smul {
smul_opp :
opp S;
_ : @
mulr_closed R S}.
@@ -3474,15 +3489,15 @@
Ltac done :=
case⇒ *;
assumption.
-
Fact zmod_oppr R S : @
zmod R S → oppr_closed S.
-
Fact semiring_mulr R S : @
semiring R S → mulr_closed S.
-
Fact smul_mulr R S : @
smul R S → mulr_closed S.
-
Fact submod_scaler R V S : @
submod R V S → scaler_closed S.
-
Fact subring_mulr R S : @
subring R S → mulr_closed S.
-
Fact sdiv_invr R S : @
sdiv R S → invr_closed S.
-
Fact subalg_scaler R A S : @
subalg R A S → scaler_closed S.
-
Fact divring_invr R S : @
divring R S → invr_closed S.
-
Fact divalg_scaler R A S : @
divalg R A S → scaler_closed S.
+
Fact zmod_oppr R S : @
zmod R S → oppr_closed S.
+
Fact semiring_mulr R S : @
semiring R S → mulr_closed S.
+
Fact smul_mulr R S : @
smul R S → mulr_closed S.
+
Fact submod_scaler R V S : @
submod R V S → scaler_closed S.
+
Fact subring_mulr R S : @
subring R S → mulr_closed S.
+
Fact sdiv_invr R S : @
sdiv R S → invr_closed S.
+
Fact subalg_scaler R A S : @
subalg R A S → scaler_closed S.
+
Fact divring_invr R S : @
divring R S → invr_closed S.
+
Fact divalg_scaler R A S : @
divalg R A S → scaler_closed S.
Definition zmod_opp R S (
addS : @
zmod R S) :=
@@ -3517,33 +3532,33 @@
-
Lemma opp_ext (
U :
zmodType)
S k (
kS : @
keyed_pred U S k) :
-
oppr_closed kS → oppr_closed S.
+
Lemma opp_ext (
U :
zmodType)
S k (
kS : @
keyed_pred U S k) :
+
oppr_closed kS → oppr_closed S.
-
Lemma add_ext (
U :
zmodType)
S k (
kS : @
keyed_pred U S k) :
-
addr_closed kS → addr_closed S.
+
Lemma add_ext (
U :
zmodType)
S k (
kS : @
keyed_pred U S k) :
+
addr_closed kS → addr_closed S.
-
Lemma mul_ext (
R :
ringType)
S k (
kS : @
keyed_pred R S k) :
-
mulr_closed kS → mulr_closed S.
+
Lemma mul_ext (
R :
ringType)
S k (
kS : @
keyed_pred R S k) :
+
mulr_closed kS → mulr_closed S.
-
Lemma scale_ext (
R :
ringType) (
U :
lmodType R)
S k (
kS : @
keyed_pred U S k) :
-
scaler_closed kS → scaler_closed S.
+
Lemma scale_ext (
R :
ringType) (
U :
lmodType R)
S k (
kS : @
keyed_pred U S k) :
+
scaler_closed kS → scaler_closed S.
-
Lemma inv_ext (
R :
unitRingType)
S k (
kS : @
keyed_pred R S k) :
-
invr_closed kS → invr_closed S.
+
Lemma inv_ext (
R :
unitRingType)
S k (
kS : @
keyed_pred R S k) :
+
invr_closed kS → invr_closed S.
End Extensionality.
Module Default.
-
Definition opp V S oppS := @
Opp V S (
DefaultPredKey S)
oppS.
-
Definition add V S addS := @
Add V S (
DefaultPredKey S)
addS.
-
Definition mul R S mulS := @
Mul R S (
DefaultPredKey S)
mulS.
+
Definition opp V S oppS := @
Opp V S (
DefaultPredKey S)
oppS.
+
Definition add V S addS := @
Add V S (
DefaultPredKey S)
addS.
+
Definition mul R S mulS := @
Mul R S (
DefaultPredKey S)
mulS.
Definition zmod V S addS oppS := @
Zmod V S (
add addS)
oppS.
Definition semiring R S addS mulS := @
Semiring R S (
add addS)
mulS.
Definition smul R S oppS mulS := @
Smul R S (
opp oppS)
mulS.
@@ -3700,29 +3715,29 @@
Section ZmodulePred.
-
Variables (
V :
zmodType) (
S :
predPredType V).
+
Variables (
V :
zmodType) (
S :
{pred V}).
Section Add.
-
Variables (
addS :
addrPred S) (
kS :
keyed_pred addS).
+
Variables (
addS :
addrPred S) (
kS :
keyed_pred addS).
Lemma rpred0D :
addr_closed kS.
-
Lemma rpred0 : 0
\in kS.
+
Lemma rpred0 : 0
\in kS.
-
Lemma rpredD :
{in kS &, ∀ u v,
u + v \in kS}.
+
Lemma rpredD :
{in kS &, ∀ u v,
u + v \in kS}.
-
Lemma rpred_sum I r (
P :
pred I)
F :
-
(∀ i,
P i → F i \in kS) → \sum_(i <- r | P i) F i \in kS.
+
Lemma rpred_sum I r (
P :
pred I)
F :
+
(∀ i,
P i → F i \in kS) → \sum_(i <- r | P i) F i \in kS.
-
Lemma rpredMn n :
{in kS, ∀ u,
u *+ n \in kS}.
+
Lemma rpredMn n :
{in kS, ∀ u,
u *+ n \in kS}.
End Add.
@@ -3731,13 +3746,13 @@
Section Opp.
-
Variables (
oppS :
opprPred S) (
kS :
keyed_pred oppS).
+
Variables (
oppS :
opprPred S) (
kS :
keyed_pred oppS).
Lemma rpredNr :
oppr_closed kS.
-
Lemma rpredN :
{mono -%R: u / u \in kS}.
+
Lemma rpredN :
{mono -%R: u / u \in kS}.
End Opp.
@@ -3746,25 +3761,25 @@
Section Sub.
-
Variables (
subS :
zmodPred S) (
kS :
keyed_pred subS).
+
Variables (
subS :
zmodPred S) (
kS :
keyed_pred subS).
-
Lemma rpredB :
{in kS &, ∀ u v,
u - v \in kS}.
+
Lemma rpredB :
{in kS &, ∀ u v,
u - v \in kS}.
-
Lemma rpredMNn n :
{in kS, ∀ u,
u *- n \in kS}.
+
Lemma rpredMNn n :
{in kS, ∀ u,
u *- n \in kS}.
-
Lemma rpredDr x y :
x \in kS → (y + x \in kS) = (y \in kS).
+
Lemma rpredDr x y :
x \in kS → (y + x \in kS) = (y \in kS).
-
Lemma rpredDl x y :
x \in kS → (x + y \in kS) = (y \in kS).
+
Lemma rpredDl x y :
x \in kS → (x + y \in kS) = (y \in kS).
-
Lemma rpredBr x y :
x \in kS → (y - x \in kS) = (y \in kS).
+
Lemma rpredBr x y :
x \in kS → (y - x \in kS) = (y \in kS).
-
Lemma rpredBl x y :
x \in kS → (x - y \in kS) = (y \in kS).
+
Lemma rpredBl x y :
x \in kS → (x - y \in kS) = (y \in kS).
End Sub.
@@ -3776,46 +3791,46 @@
Section RingPred.
-
Variables (
R :
ringType) (
S :
predPredType R).
+
Variables (
R :
ringType) (
S :
{pred R}).
-
Lemma rpredMsign (
oppS :
opprPred S) (
kS :
keyed_pred oppS)
n x :
-
((-1
) ^+ n × x \in kS) = (x \in kS).
+
Lemma rpredMsign (
oppS :
opprPred S) (
kS :
keyed_pred oppS)
n x :
+
((-1
) ^+ n × x \in kS) = (x \in kS).
Section Mul.
-
Variables (
mulS :
mulrPred S) (
kS :
keyed_pred mulS).
+
Variables (
mulS :
mulrPred S) (
kS :
keyed_pred mulS).
Lemma rpred1M :
mulr_closed kS.
-
Lemma rpred1 : 1
\in kS.
+
Lemma rpred1 : 1
\in kS.
-
Lemma rpredM :
{in kS &, ∀ u v,
u × v \in kS}.
+
Lemma rpredM :
{in kS &, ∀ u v,
u × v \in kS}.
-
Lemma rpred_prod I r (
P :
pred I)
F :
-
(∀ i,
P i → F i \in kS) → \prod_(i <- r | P i) F i \in kS.
+
Lemma rpred_prod I r (
P :
pred I)
F :
+
(∀ i,
P i → F i \in kS) → \prod_(i <- r | P i) F i \in kS.
-
Lemma rpredX n :
{in kS, ∀ u,
u ^+ n \in kS}.
+
Lemma rpredX n :
{in kS, ∀ u,
u ^+ n \in kS}.
End Mul.
-
Lemma rpred_nat (
rngS :
semiringPred S) (
kS :
keyed_pred rngS)
n :
n%:R \in kS.
+
Lemma rpred_nat (
rngS :
semiringPred S) (
kS :
keyed_pred rngS)
n :
n%:R \in kS.
-
Lemma rpredN1 (
mulS :
smulrPred S) (
kS :
keyed_pred mulS) : -1
\in kS.
+
Lemma rpredN1 (
mulS :
smulrPred S) (
kS :
keyed_pred mulS) : -1
\in kS.
-
Lemma rpred_sign (
mulS :
smulrPred S) (
kS :
keyed_pred mulS)
n :
-
(-1
) ^+ n \in kS.
+
Lemma rpred_sign (
mulS :
smulrPred S) (
kS :
keyed_pred mulS)
n :
+
(-1
) ^+ n \in kS.
End RingPred.
@@ -3824,18 +3839,18 @@
Section LmodPred.
-
Variables (
R :
ringType) (
V :
lmodType R) (
S :
predPredType V).
+
Variables (
R :
ringType) (
V :
lmodType R) (
S :
{pred V}).
-
Lemma rpredZsign (
oppS :
opprPred S) (
kS :
keyed_pred oppS)
n u :
-
((-1
) ^+ n *: u \in kS) = (u \in kS).
+
Lemma rpredZsign (
oppS :
opprPred S) (
kS :
keyed_pred oppS)
n u :
+
((-1
) ^+ n *: u \in kS) = (u \in kS).
-
Lemma rpredZnat (
addS :
addrPred S) (
kS :
keyed_pred addS)
n :
-
{in kS, ∀ u,
n%:R *: u \in kS}.
+
Lemma rpredZnat (
addS :
addrPred S) (
kS :
keyed_pred addS)
n :
+
{in kS, ∀ u,
n%:R *: u \in kS}.
-
Lemma rpredZ (
linS :
submodPred S) (
kS :
keyed_pred linS) :
scaler_closed kS.
+
Lemma rpredZ (
linS :
submodPred S) (
kS :
keyed_pred linS) :
scaler_closed kS.
End LmodPred.
@@ -3850,31 +3865,31 @@
Section Div.
-
Variables (
S :
predPredType R) (
divS :
divrPred S) (
kS :
keyed_pred divS).
+
Variables (
S :
{pred R}) (
divS :
divrPred S) (
kS :
keyed_pred divS).
-
Lemma rpredVr x :
x \in kS → x^-1 \in kS.
+
Lemma rpredVr x :
x \in kS → x^-1 \in kS.
-
Lemma rpredV x :
(x^-1 \in kS) = (x \in kS).
+
Lemma rpredV x :
(x^-1 \in kS) = (x \in kS).
-
Lemma rpred_div :
{in kS &, ∀ x y,
x / y \in kS}.
+
Lemma rpred_div :
{in kS &, ∀ x y,
x / y \in kS}.
-
Lemma rpredXN n :
{in kS, ∀ x,
x ^- n \in kS}.
+
Lemma rpredXN n :
{in kS, ∀ x,
x ^- n \in kS}.
-
Lemma rpredMl x y :
x \in kS → x \is a unit→ (x × y \in kS) = (y \in kS).
+
Lemma rpredMl x y :
x \in kS → x \is a unit→ (x × y \in kS) = (y \in kS).
-
Lemma rpredMr x y :
x \in kS → x \is a unit → (y × x \in kS) = (y \in kS).
+
Lemma rpredMr x y :
x \in kS → x \is a unit → (y × x \in kS) = (y \in kS).
-
Lemma rpred_divr x y :
x \in kS → x \is a unit → (y / x \in kS) = (y \in kS).
+
Lemma rpred_divr x y :
x \in kS → x \is a unit → (y / x \in kS) = (y \in kS).
-
Lemma rpred_divl x y :
x \in kS → x \is a unit → (x / y \in kS) = (y \in kS).
+
Lemma rpred_divl x y :
x \in kS → x \is a unit → (x / y \in kS) = (y \in kS).
End Div.
@@ -3893,17 +3908,17 @@
Implicit Type x :
R.
-
Lemma unitrN x :
(- x \is a unit) = (x \is a unit).
+
Lemma unitrN x :
(- x \is a unit) = (x \is a unit).
-
Lemma invrN x :
(- x)^-1 = - x^-1.
+
Lemma invrN x :
(- x)^-1 = - x^-1.
-
Lemma invr_signM n x :
((-1
) ^+ n × x)^-1 = (-1
) ^+ n × x^-1.
+
Lemma invr_signM n x :
((-1
) ^+ n × x)^-1 = (-1
) ^+ n × x^-1.
-
Lemma divr_signM (
b1 b2 :
bool)
x1 x2:
-
((-1
) ^+ b1 × x1) / ((-1
) ^+ b2 × x2) = (-1
) ^+ (b1 (+) b2) × (x1 / x2).
+
Lemma divr_signM (
b1 b2 :
bool)
x1 x2:
+
((-1
) ^+ b1 × x1) / ((-1
) ^+ b2 × x2) = (-1
) ^+ (b1 (+) b2) × (x1 / x2).
End UnitRingPred.
@@ -3922,27 +3937,27 @@
Inductive term :
Type :=
-|
Var of nat
+|
Var of nat
|
Const of R
-|
NatConst of nat
+|
NatConst of nat
|
Add of term &
term
|
Opp of term
-|
NatMul of term &
nat
+|
NatMul of term &
nat
|
Mul of term &
term
|
Inv of term
-|
Exp of term &
nat.
+|
Exp of term &
nat.
Inductive formula :
Type :=
-|
Bool of bool
+|
Bool of bool
|
Equal of term &
term
|
Unit of term
|
And of formula &
formula
|
Or of formula &
formula
|
Implies of formula &
formula
|
Not of formula
-|
Exists of nat &
formula
-|
Forall of nat &
formula.
+|
Exists of nat &
formula
+|
Forall of nat &
formula.
End TermDef.
@@ -3952,8 +3967,8 @@
-
Notation True := (
Bool true).
-
Notation False := (
Bool false).
+
Notation True := (
Bool true).
+
Notation False := (
Bool false).
@@ -3964,30 +3979,30 @@
Variable R :
Type.
-
Fixpoint tsubst (
t :
term R) (
s :
nat × term R) :=
+
Fixpoint tsubst (
t :
term R) (
s :
nat × term R) :=
match t with
- |
'X_i ⇒
if i == s.1 then s.2 else t
- |
_%:T |
_%:R ⇒
t
- |
t1 + t2 ⇒
tsubst t1 s + tsubst t2 s
- |
- t1 ⇒
- tsubst t1 s
- |
t1 *+ n ⇒
tsubst t1 s *+ n
- |
t1 × t2 ⇒
tsubst t1 s × tsubst t2 s
- |
t1^-1 ⇒
(tsubst t1 s)^-1
- |
t1 ^+ n ⇒
tsubst t1 s ^+ n
+ |
'X_i ⇒
if i == s.1 then s.2 else t
+ |
_%:T |
_%:R ⇒
t
+ |
t1 + t2 ⇒
tsubst t1 s + tsubst t2 s
+ |
- t1 ⇒
- tsubst t1 s
+ |
t1 *+ n ⇒
tsubst t1 s *+ n
+ |
t1 × t2 ⇒
tsubst t1 s × tsubst t2 s
+ |
t1^-1 ⇒
(tsubst t1 s)^-1
+ |
t1 ^+ n ⇒
tsubst t1 s ^+ n
end%
T.
-
Fixpoint fsubst (
f :
formula R) (
s :
nat × term R) :=
+
Fixpoint fsubst (
f :
formula R) (
s :
nat × term R) :=
match f with
|
Bool _ ⇒
f
- |
t1 == t2 ⇒
tsubst t1 s == tsubst t2 s
+ |
t1 == t2 ⇒
tsubst t1 s == tsubst t2 s
|
Unit t1 ⇒
Unit (
tsubst t1 s)
- |
f1 ∧ f2 ⇒
fsubst f1 s ∧ fsubst f2 s
- |
f1 ∨ f2 ⇒
fsubst f1 s ∨ fsubst f2 s
- |
f1 ==> f2 ⇒
fsubst f1 s ==> fsubst f2 s
- |
¬ f1 ⇒
¬ fsubst f1 s
- | (
'∃ 'X_i, f1) ⇒
'∃ 'X_i, if i == s.1 then f1 else fsubst f1 s
- | (
'∀ 'X_i, f1) ⇒
'∀ 'X_i, if i == s.1 then f1 else fsubst f1 s
+ |
f1 ∧ f2 ⇒
fsubst f1 s ∧ fsubst f2 s
+ |
f1 ∨ f2 ⇒
fsubst f1 s ∨ fsubst f2 s
+ |
f1 ==> f2 ⇒
fsubst f1 s ==> fsubst f2 s
+ |
¬ f1 ⇒
¬ fsubst f1 s
+ | (
'∃ 'X_i, f1) ⇒
'∃ 'X_i, if i == s.1 then f1 else fsubst f1 s
+ | (
'∀ 'X_i, f1) ⇒
'∀ 'X_i, if i == s.1 then f1 else fsubst f1 s
end%
T.
@@ -4008,26 +4023,26 @@
@@ -4039,18 +4054,18 @@
Fixpoint holds (
e :
seq R) (
f :
formula R) {
struct f} :
Prop :=
match f with
|
Bool b ⇒
b
- | (
t1 == t2)%
T ⇒
eval e t1 = eval e t2
- |
Unit t1 ⇒
eval e t1 \in unit
- | (
f1 ∧ f2)%
T ⇒
holds e f1 ∧ holds e f2
- | (
f1 ∨ f2)%
T ⇒
holds e f1 ∨ holds e f2
- | (
f1 ==> f2)%
T ⇒
holds e f1 → holds e f2
- | (
¬ f1)%
T ⇒
¬ holds e f1
- | (
'∃ 'X_i, f1)%
T ⇒
∃ x, holds (
set_nth 0
e i x)
f1
- | (
'∀ 'X_i, f1)%
T ⇒
∀ x,
holds (
set_nth 0
e i x)
f1
+ | (
t1 == t2)%
T ⇒
eval e t1 = eval e t2
+ |
Unit t1 ⇒
eval e t1 \in unit
+ | (
f1 ∧ f2)%
T ⇒
holds e f1 ∧ holds e f2
+ | (
f1 ∨ f2)%
T ⇒
holds e f1 ∨ holds e f2
+ | (
f1 ==> f2)%
T ⇒
holds e f1 → holds e f2
+ | (
¬ f1)%
T ⇒
¬ holds e f1
+ | (
'∃ 'X_i, f1)%
T ⇒
∃ x, holds (
set_nth 0
e i x)
f1
+ | (
'∀ 'X_i, f1)%
T ⇒
∀ x,
holds (
set_nth 0
e i x)
f1
end.
-
Lemma same_env_sym e e' :
same_env e e' → same_env e' e.
+
Lemma same_env_sym e e' :
same_env e e' → same_env e' e.
@@ -4059,7 +4074,7 @@
Extensionality of formula evaluation
@@ -4069,7 +4084,7 @@
@@ -4080,10 +4095,10 @@
Fixpoint rterm (
t :
term R) :=
match t with
- |
_^-1 ⇒
false
- |
t1 + t2 |
t1 × t2 ⇒
rterm t1 && rterm t2
- |
- t1 |
t1 *+ _ |
t1 ^+ _ ⇒
rterm t1
- |
_ ⇒
true
+ |
_^-1 ⇒
false
+ |
t1 + t2 |
t1 × t2 ⇒
rterm t1 && rterm t2
+ |
- t1 |
t1 *+ _ |
t1 ^+ _ ⇒
rterm t1
+ |
_ ⇒
true
end%
T.
@@ -4095,11 +4110,11 @@
Fixpoint rformula (
f :
formula R) :=
match f with
- |
Bool _ ⇒
true
- |
t1 == t2 ⇒
rterm t1 && rterm t2
- |
Unit t1 ⇒
false
- |
f1 ∧ f2 |
f1 ∨ f2 |
f1 ==> f2 ⇒
rformula f1 && rformula f2
- |
¬ f1 | (
'∃ 'X__, f1) | (
'∀ 'X__, f1) ⇒
rformula f1
+ |
Bool _ ⇒
true
+ |
t1 == t2 ⇒
rterm t1 && rterm t2
+ |
Unit t1 ⇒
false
+ |
f1 ∧ f2 |
f1 ∨ f2 |
f1 ==> f2 ⇒
rformula f1 && rformula f2
+ |
¬ f1 | (
'∃ 'X__, f1) | (
'∀ 'X__, f1) ⇒
rformula f1
end%
T.
@@ -4111,9 +4126,9 @@
-
Fixpoint to_rterm (
t :
term R) (
r :
seq (
term R)) (
n :
nat) {
struct t} :=
+
Fixpoint to_rterm (
t :
term R) (
r :
seq (
term R)) (
n :
nat) {
struct t} :=
match t with
- |
t1^-1 ⇒
-
let:
(t1', r1) :=
to_rterm t1 r n in
-
('X_(n + size r1), rcons r1 t1')
- |
t1 + t2 ⇒
-
let:
(t1', r1) :=
to_rterm t1 r n in
-
let:
(t2', r2) :=
to_rterm t2 r1 n in
-
(t1' + t2', r2)
- |
- t1 ⇒
-
let:
(t1', r1) :=
to_rterm t1 r n in
-
(- t1', r1)
- |
t1 *+ m ⇒
-
let:
(t1', r1) :=
to_rterm t1 r n in
-
(t1' *+ m, r1)
- |
t1 × t2 ⇒
-
let:
(t1', r1) :=
to_rterm t1 r n in
-
let:
(t2', r2) :=
to_rterm t2 r1 n in
-
(Mul t1' t2', r2)
- |
t1 ^+ m ⇒
-
let:
(t1', r1) :=
to_rterm t1 r n in
-
(t1' ^+ m, r1)
- |
_ ⇒
(t, r)
+ |
t1^-1 ⇒
+
let:
(t1', r1) :=
to_rterm t1 r n in
+
('X_(n + size r1), rcons r1 t1')
+ |
t1 + t2 ⇒
+
let:
(t1', r1) :=
to_rterm t1 r n in
+
let:
(t2', r2) :=
to_rterm t2 r1 n in
+
(t1' + t2', r2)
+ |
- t1 ⇒
+
let:
(t1', r1) :=
to_rterm t1 r n in
+
(- t1', r1)
+ |
t1 *+ m ⇒
+
let:
(t1', r1) :=
to_rterm t1 r n in
+
(t1' *+ m, r1)
+ |
t1 × t2 ⇒
+
let:
(t1', r1) :=
to_rterm t1 r n in
+
let:
(t2', r2) :=
to_rterm t2 r1 n in
+
(Mul t1' t2', r2)
+ |
t1 ^+ m ⇒
+
let:
(t1', r1) :=
to_rterm t1 r n in
+
(t1' ^+ m, r1)
+ |
_ ⇒
(t, r)
end%
T.
-
Lemma to_rterm_id t r n :
rterm t → to_rterm t r n = (t, r).
+
Lemma to_rterm_id t r n :
rterm t → to_rterm t r n = (t, r).
@@ -4163,12 +4178,12 @@
Definition eq0_rform t1 :=
let m :=
ub_var t1 in
-
let:
(t1', r1) :=
to_rterm t1 [::] m in
+
let:
(t1', r1) :=
to_rterm t1 [::] m in
let fix loop r i :=
match r with
- |
[::] ⇒
t1' == 0
- |
t :: r' ⇒
-
let f :=
'X_i × t == 1
∧ t × 'X_i == 1
in
-
'∀ 'X_i, (f ∨ 'X_i == t ∧ ¬ ('∃ 'X_i, f)) ==> loop r' i.+1
+ |
[::] ⇒
t1' == 0
+ |
t :: r' ⇒
+
let f :=
'X_i × t == 1
∧ t × 'X_i == 1
in
+
'∀ 'X_i, (f ∨ 'X_i == t ∧ ¬ ('∃ 'X_i, f)) ==> loop r' i.+1
end%
T
in loop r1 m.
@@ -4183,14 +4198,14 @@
Fixpoint to_rform f :=
match f with
|
Bool b ⇒
f
- |
t1 == t2 ⇒
eq0_rform (
t1 - t2)
- |
Unit t1 ⇒
eq0_rform (
t1 × t1^-1 - 1)
- |
f1 ∧ f2 ⇒
to_rform f1 ∧ to_rform f2
- |
f1 ∨ f2 ⇒
to_rform f1 ∨ to_rform f2
- |
f1 ==> f2 ⇒
to_rform f1 ==> to_rform f2
- |
¬ f1 ⇒
¬ to_rform f1
- | (
'∃ 'X_i, f1) ⇒
'∃ 'X_i, to_rform f1
- | (
'∀ 'X_i, f1) ⇒
'∀ 'X_i, to_rform f1
+ |
t1 == t2 ⇒
eq0_rform (
t1 - t2)
+ |
Unit t1 ⇒
eq0_rform (
t1 × t1^-1 - 1)
+ |
f1 ∧ f2 ⇒
to_rform f1 ∧ to_rform f2
+ |
f1 ∨ f2 ⇒
to_rform f1 ∨ to_rform f2
+ |
f1 ==> f2 ⇒
to_rform f1 ==> to_rform f2
+ |
¬ f1 ⇒
¬ to_rform f1
+ | (
'∃ 'X_i, f1) ⇒
'∃ 'X_i, to_rform f1
+ | (
'∀ 'X_i, f1) ⇒
'∀ 'X_i, to_rform f1
end%
T.
@@ -4209,7 +4224,7 @@
Correctness of the transformation.
@@ -4224,10 +4239,10 @@
@@ -4274,8 +4289,8 @@
@@ -4284,16 +4299,16 @@
Computes a DNF from a qf ring formula
-
Fixpoint qf_to_dnf (
f :
formula R) (
neg :
bool) {
struct f} :=
+
Fixpoint qf_to_dnf (
f :
formula R) (
neg :
bool) {
struct f} :=
match f with
- |
Bool b ⇒
if b (+) neg then [:: ([::], [::])] else [::]
- |
t1 == t2 ⇒
[:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
- |
f1 ∧ f2 ⇒ (
if neg then cat else and_dnf)
[rec f1, neg] [rec f2, neg]
- |
f1 ∨ f2 ⇒ (
if neg then and_dnf else cat)
[rec f1, neg] [rec f2, neg]
- |
f1 ==> f2 ⇒ (
if neg then and_dnf else cat)
[rec f1, ~~ neg] [rec f2, neg]
- |
¬ f1 ⇒
[rec f1, ~~ neg]
- |
_ ⇒
if neg then [:: ([::], [::])] else [::]
-
end%
T where "[ 'rec' f , neg ]" := (
qf_to_dnf f neg).
+ |
Bool b ⇒
if b (+) neg then [:: ([::], [::])] else [::]
+ |
t1 == t2 ⇒
[:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
+ |
f1 ∧ f2 ⇒ (
if neg then cat else and_dnf)
[rec f1, neg] [rec f2, neg]
+ |
f1 ∨ f2 ⇒ (
if neg then and_dnf else cat)
[rec f1, neg] [rec f2, neg]
+ |
f1 ==> f2 ⇒ (
if neg then and_dnf else cat)
[rec f1, ~~ neg] [rec f2, neg]
+ |
¬ f1 ⇒
[rec f1, ~~ neg]
+ |
_ ⇒
if neg then [:: ([::], [::])] else [::]
+
end%
T where "[ 'rec' f , neg ]" := (
qf_to_dnf f neg).
@@ -4303,8 +4318,8 @@
Lemma and_dnfP e bcs1 bcs2 :
qf_eval e (
dnf_to_form (
and_dnf bcs1 bcs2))
-
= qf_eval e (
dnf_to_form bcs1 ∧ dnf_to_form bcs2).
+
= qf_eval e (
dnf_to_form bcs1 ∧ dnf_to_form bcs2).
Lemma qf_to_dnfP e :
let qev f b :=
qf_eval e (
dnf_to_form (
qf_to_dnf f b))
in
-
∀ f,
qf_form f && rformula f → qev f false = qf_eval e f.
+
∀ f,
qf_form f && rformula f → qev f false = qf_eval e f.
Lemma dnf_to_form_qf bcs :
qf_form (
dnf_to_form bcs).
-
Definition dnf_rterm cl :=
all rterm cl.1 && all rterm cl.2.
+
Definition dnf_rterm cl :=
all rterm cl.1 && all rterm cl.2.
-
Lemma qf_to_dnf_rterm f b :
rformula f → all dnf_rterm (
qf_to_dnf f b).
+
Lemma qf_to_dnf_rterm f b :
rformula f → all dnf_rterm (
qf_to_dnf f b).
-
Lemma dnf_to_rform bcs :
rformula (
dnf_to_form bcs)
= all dnf_rterm bcs.
+
Lemma dnf_to_rform bcs :
rformula (
dnf_to_form bcs)
= all dnf_rterm bcs.
Section If.
@@ -4353,19 +4368,19 @@
Variables (
pred_f then_f else_f :
formula R).
-
Definition If := (
pred_f ∧ then_f ∨ ¬ pred_f ∧ else_f)%
T.
+
Definition If := (
pred_f ∧ then_f ∨ ¬ pred_f ∧ else_f)%
T.
Lemma If_form_qf :
-
qf_form pred_f → qf_form then_f → qf_form else_f → qf_form If.
+
qf_form pred_f → qf_form then_f → qf_form else_f → qf_form If.
Lemma If_form_rf :
-
rformula pred_f → rformula then_f → rformula else_f → rformula If.
+
rformula pred_f → rformula then_f → rformula else_f → rformula If.
Lemma eval_If e :
-
let ev :=
qf_eval e in ev If = (if ev pred_f then ev then_f else ev else_f).
+
let ev :=
qf_eval e in ev If = (if ev pred_f then ev then_f else ev else_f).
End If.
@@ -4374,25 +4389,25 @@
Section Pick.
-
Variables (
I :
finType) (
pred_f then_f :
I → formula R) (
else_f :
formula R).
+
Variables (
I :
finType) (
pred_f then_f :
I → formula R) (
else_f :
formula R).
Definition Pick :=
-
\big[Or/False]_(p : {ffun pred I})
- (
(\big[And/True]_i (if p i then pred_f i else ¬ pred_f i))
-
∧ (if pick p is Some i then then_f i else else_f))%
T.
+
\big[Or/False]_(p : {ffun pred I})
+ (
(\big[And/True]_i (if p i then pred_f i else ¬ pred_f i))
+
∧ (if pick p is Some i then then_f i else else_f))%
T.
Lemma Pick_form_qf :
-
(∀ i,
qf_form (
pred_f i)
) →
-
(∀ i,
qf_form (
then_f i)
) →
-
qf_form else_f →
+
(∀ i,
qf_form (
pred_f i)
) →
+
(∀ i,
qf_form (
then_f i)
) →
+
qf_form else_f →
qf_form Pick.
Lemma eval_Pick e (
qev :=
qf_eval e) :
let P i :=
qev (
pred_f i)
in
-
qev Pick = (if pick P is Some i then qev (
then_f i)
else qev else_f).
+
qev Pick = (if pick P is Some i then qev (
then_f i)
else qev else_f).
End Pick.
@@ -4402,17 +4417,17 @@
Variable f :
formula R.
-
Implicit Types (
I :
seq nat) (
e :
seq R).
+
Implicit Types (
I :
seq nat) (
e :
seq R).
Lemma foldExistsP I e :
-
(exists2 e', {in [predC I], same_env e e'} & holds e' f)
-
↔ holds e (
foldr Exists f I).
+
(exists2 e', {in [predC I], same_env e e'} & holds e' f)
+
↔ holds e (
foldr Exists f I).
Lemma foldForallP I e :
-
(∀ e',
{in [predC I], same_env e e'} → holds e' f)
-
↔ holds e (
foldr Forall f I).
+
(∀ e',
{in [predC I], same_env e e'} → holds e' f)
+
↔ holds e (
foldr Forall f I).
End MultiQuant.
@@ -4427,36 +4442,36 @@
Definition axiom (
R :
ringType) :=
-
∀ x y :
R,
x × y = 0
→ (x == 0
) || (y == 0
).
+
∀ x y :
R,
x × y = 0
→ (x == 0
) || (y == 0
).
Section ClassDef.
Record class_of (
R :
Type) :
Type :=
-
Class {
base :
ComUnitRing.class_of R;
mixin :
axiom (
Ring.Pack base R)}.
+
Class {
base :
ComUnitRing.class_of R;
mixin :
axiom (
Ring.Pack base)}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variable (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack b0 (
m0 :
axiom (@
Ring.Pack T b0 T)) :=
-
fun bT b &
phant_id (
ComUnitRing.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
Definition pack b0 (
m0 :
axiom (@
Ring.Pack T b0)) :=
+
fun bT b &
phant_id (
ComUnitRing.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass.
End ClassDef.
@@ -4481,10 +4496,10 @@
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Notation idomainType :=
type.
-
Notation IdomainType T m := (@
pack T _ m _ _ id _ id).
-
Notation "[ 'idomainType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation IdomainType T m := (@
pack T _ m _ _ id _ id).
+
Notation "[ 'idomainType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'idomainType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'idomainType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'idomainType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'idomainType' 'of' T ]") :
form_scope.
End Exports.
@@ -4500,78 +4515,78 @@
Implicit Types x y :
R.
-
Lemma mulf_eq0 x y :
(x × y == 0
) = (x == 0
) || (y == 0
).
+
Lemma mulf_eq0 x y :
(x × y == 0
) = (x == 0
) || (y == 0
).
-
Lemma prodf_eq0 (
I :
finType) (
P :
pred I) (
F :
I → R) :
-
reflect (
exists2 i, P i & (F i == 0
)) (
\prod_(i | P i) F i == 0).
+
Lemma prodf_eq0 (
I :
finType) (
P :
pred I) (
F :
I → R) :
+
reflect (
exists2 i, P i & (F i == 0
)) (
\prod_(i | P i) F i == 0).
-
Lemma prodf_seq_eq0 I r (
P :
pred I) (
F :
I → R) :
-
(\prod_(i <- r | P i) F i == 0
) = has (
fun i ⇒
P i && (F i == 0
))
r.
+
Lemma prodf_seq_eq0 I r (
P :
pred I) (
F :
I → R) :
+
(\prod_(i <- r | P i) F i == 0
) = has (
fun i ⇒
P i && (F i == 0
))
r.
-
Lemma mulf_neq0 x y :
x != 0
→ y != 0
→ x × y != 0.
+
Lemma mulf_neq0 x y :
x != 0
→ y != 0
→ x × y != 0.
-
Lemma prodf_neq0 (
I :
finType) (
P :
pred I) (
F :
I → R) :
-
reflect (
∀ i,
P i → (F i != 0
)) (
\prod_(i | P i) F i != 0).
+
Lemma prodf_neq0 (
I :
finType) (
P :
pred I) (
F :
I → R) :
+
reflect (
∀ i,
P i → (F i != 0
)) (
\prod_(i | P i) F i != 0).
-
Lemma prodf_seq_neq0 I r (
P :
pred I) (
F :
I → R) :
-
(\prod_(i <- r | P i) F i != 0
) = all (
fun i ⇒
P i ==> (F i != 0
))
r.
+
Lemma prodf_seq_neq0 I r (
P :
pred I) (
F :
I → R) :
+
(\prod_(i <- r | P i) F i != 0
) = all (
fun i ⇒
P i ==> (F i != 0
))
r.
-
Lemma expf_eq0 x n :
(x ^+ n == 0
) = (n > 0
) && (x == 0
).
+
Lemma expf_eq0 x n :
(x ^+ n == 0
) = (n > 0
) && (x == 0
).
-
Lemma sqrf_eq0 x :
(x ^+ 2
== 0
) = (x == 0
).
+
Lemma sqrf_eq0 x :
(x ^+ 2
== 0
) = (x == 0
).
-
Lemma expf_neq0 x m :
x != 0
→ x ^+ m != 0.
+
Lemma expf_neq0 x m :
x != 0
→ x ^+ m != 0.
-
Lemma natf_neq0 n :
(n%:R != 0
:> R) = [char R]^'.-nat n.
+
Lemma natf_neq0 n :
(n%:R != 0
:> R) = [char R]^'.-nat n.
-
Lemma natf0_char n :
n > 0
→ n%:R == 0
:> R → ∃ p, p \in [char R].
+
Lemma natf0_char n :
n > 0
→ n%:R == 0
:> R → ∃ p, p \in [char R].
-
Lemma charf'_nat n :
[char R]^'.-nat n = (n%:R != 0
:> R).
+
Lemma charf'_nat n :
[char R]^'.-nat n = (n%:R != 0
:> R).
-
Lemma charf0P :
[char R] =i pred0 ↔ (∀ n,
(n%:R == 0
:> R) = (
n == 0)%
N).
+
Lemma charf0P :
[char R] =i pred0 ↔ (∀ n,
(n%:R == 0
:> R) = (
n == 0)%
N).
-
Lemma eqf_sqr x y :
(x ^+ 2
== y ^+ 2
) = (x == y) || (x == - y).
+
Lemma eqf_sqr x y :
(x ^+ 2
== y ^+ 2
) = (x == y) || (x == - y).
-
Lemma mulfI x :
x != 0
→ injective (
*%R x).
+
Lemma mulfI x :
x != 0
→ injective (
*%R x).
-
Lemma mulIf x :
x != 0
→ injective (
*%R^~ x).
+
Lemma mulIf x :
x != 0
→ injective (
*%R^~ x).
-
Lemma divfI x :
x != 0
→ injective (
fun y ⇒
x / y).
+
Lemma divfI x :
x != 0
→ injective (
fun y ⇒
x / y).
-
Lemma divIf y :
y != 0
→ injective (
fun x ⇒
x / y).
+
Lemma divIf y :
y != 0
→ injective (
fun x ⇒
x / y).
-
Lemma sqrf_eq1 x :
(x ^+ 2
== 1
) = (x == 1
) || (x == -1
).
+
Lemma sqrf_eq1 x :
(x ^+ 2
== 1
) = (x == 1
) || (x == -1
).
Lemma expfS_eq1 x n :
-
(x ^+ n.+1 == 1
) = (x == 1
) || (\sum_(i < n.+1) x ^+ i == 0
).
+
(x ^+ n.+1 == 1
) = (x == 1
) || (\sum_(i < n.+1) x ^+ i == 0
).
-
Lemma lregP x :
reflect (
lreg x) (
x != 0).
+
Lemma lregP x :
reflect (
lreg x) (
x != 0).
-
Lemma rregP x :
reflect (
rreg x) (
x != 0).
+
Lemma rregP x :
reflect (
rreg x) (
x != 0).
-
Canonical regular_idomainType :=
[idomainType of R^o].
+
Canonical regular_idomainType :=
[idomainType of R^o].
End IntegralDomainTheory.
@@ -4582,34 +4597,40 @@
Module Field.
-
Definition mixin_of (
F :
unitRingType) :=
∀ x :
F,
x != 0
→ x \in unit.
+
Definition mixin_of (
R :
unitRingType) :=
∀ x :
R,
x != 0
→ x \in unit.
-
Lemma IdomainMixin R :
mixin_of R → IntegralDomain.axiom R.
+
Lemma IdomainMixin R :
mixin_of R → IntegralDomain.axiom R.
Section Mixins.
-
Variables (
R :
comRingType) (
inv :
R → R).
+
Definition axiom (
R :
ringType)
inv :=
∀ x :
R,
x != 0
→ inv x × x = 1.
-
Definition axiom :=
∀ x,
x != 0
→ inv x × x = 1.
-
Hypothesis mulVx :
axiom.
-
Hypothesis inv0 :
inv 0
= 0.
+
Variables (
R :
comRingType) (
inv :
R → R).
+
Hypotheses (
mulVf :
axiom inv) (
inv0 :
inv 0
= 0).
-
Fact intro_unit (
x y :
R) :
y × x = 1
→ x != 0.
+
Fact intro_unit (
x y :
R) :
y × x = 1
→ x != 0.
-
Fact inv_out :
{in predC (
predC1 0)
, inv =1 id}.
+
Fact inv_out :
{in predC (
predC1 0)
, inv =1 id}.
-
Definition UnitMixin :=
ComUnitRing.Mixin mulVx intro_unit inv_out.
+
Definition UnitMixin :=
ComUnitRing.Mixin mulVf intro_unit inv_out.
-
Lemma Mixin :
mixin_of (
UnitRing.Pack (
UnitRing.Class UnitMixin)
R).
-
+
Definition UnitRingType :=
[comUnitRingType of UnitRingType R UnitMixin].
+
+
+
Definition IdomainType :=
+
IdomainType UnitRingType (@
IdomainMixin UnitRingType (
fun ⇒ id)).
+
+
+
Lemma Mixin :
mixin_of IdomainType.
+
End Mixins.
@@ -4619,31 +4640,31 @@
Record class_of (
F :
Type) :
Type :=
Class {
base :
IntegralDomain.class_of F;
-
mixin :
mixin_of (
UnitRing.Pack base F)
+
mixin :
mixin_of (
UnitRing.Pack base)
}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variable (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack b0 (
m0 :
mixin_of (@
UnitRing.Pack T b0 T)) :=
-
fun bT b &
phant_id (
IntegralDomain.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
Definition pack b0 (
m0 :
mixin_of (@
UnitRing.Pack T b0)) :=
+
fun bT b &
phant_id (
IntegralDomain.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
IntegralDomain.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
IntegralDomain.Pack cT xclass.
End ClassDef.
@@ -4670,13 +4691,13 @@
Coercion idomainType : type >-> IntegralDomain.type.
Canonical idomainType.
Notation fieldType :=
type.
-
Notation FieldType T m := (@
pack T _ m _ _ id _ id).
+
Notation FieldType T m := (@
pack T _ m _ _ id _ id).
Notation FieldUnitMixin :=
UnitMixin.
Notation FieldIdomainMixin :=
IdomainMixin.
Notation FieldMixin :=
Mixin.
-
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'fieldType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'fieldType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'fieldType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'fieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -4695,75 +4716,75 @@
Lemma fieldP :
Field.mixin_of F.
-
Lemma unitfE x :
(x \in unit) = (x != 0
).
+
Lemma unitfE x :
(x \in unit) = (x != 0
).
-
Lemma mulVf x :
x != 0
→ x^-1 × x = 1.
-
Lemma divff x :
x != 0
→ x / x = 1.
+
Lemma mulVf x :
x != 0
→ x^-1 × x = 1.
+
Lemma divff x :
x != 0
→ x / x = 1.
Definition mulfV :=
divff.
-
Lemma mulKf x :
x != 0
→ cancel (
*%R x) (
*%R x^-1).
-
Lemma mulVKf x :
x != 0
→ cancel (
*%R x^-1) (
*%R x).
-
Lemma mulfK x :
x != 0
→ cancel (
*%R^~ x) (
*%R^~ x^-1).
-
Lemma mulfVK x :
x != 0
→ cancel (
*%R^~ x^-1) (
*%R^~ x).
+
Lemma mulKf x :
x != 0
→ cancel (
*%R x) (
*%R x^-1).
+
Lemma mulVKf x :
x != 0
→ cancel (
*%R x^-1) (
*%R x).
+
Lemma mulfK x :
x != 0
→ cancel (
*%R^~ x) (
*%R^~ x^-1).
+
Lemma mulfVK x :
x != 0
→ cancel (
*%R^~ x^-1) (
*%R^~ x).
Definition divfK :=
mulfVK.
-
Lemma invfM :
{morph @
inv F : x y / x × y}.
+
Lemma invfM :
{morph @
inv F : x y / x × y}.
-
Lemma invf_div x y :
(x / y)^-1 = y / x.
+
Lemma invf_div x y :
(x / y)^-1 = y / x.
-
Lemma divKf x :
x != 0
→ involutive (
fun y ⇒
x / y).
+
Lemma divKf x :
x != 0
→ involutive (
fun y ⇒
x / y).
-
Lemma expfB_cond m n x :
(x == 0
) + n ≤ m → x ^+ (m - n) = x ^+ m / x ^+ n.
+
Lemma expfB_cond m n x :
(x == 0
) + n ≤ m → x ^+ (m - n) = x ^+ m / x ^+ n.
-
Lemma expfB m n x :
n < m → x ^+ (m - n) = x ^+ m / x ^+ n.
+
Lemma expfB m n x :
n < m → x ^+ (m - n) = x ^+ m / x ^+ n.
-
Lemma prodfV I r (
P :
pred I) (
E :
I → F) :
-
\prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- r | P i) E i)^-1.
+
Lemma prodfV I r (
P :
pred I) (
E :
I → F) :
+
\prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- r | P i) E i)^-1.
-
Lemma prodf_div I r (
P :
pred I) (
E D :
I → F) :
-
\prod_(i <- r | P i) (E i / D i) =
-
\prod_(i <- r | P i) E i / \prod_(i <- r | P i) D i.
+
Lemma prodf_div I r (
P :
pred I) (
E D :
I → F) :
+
\prod_(i <- r | P i) (E i / D i) =
+
\prod_(i <- r | P i) E i / \prod_(i <- r | P i) D i.
-
Lemma telescope_prodf n m (
f :
nat → F) :
-
(∀ k,
n < k < m → f k != 0
) → n < m →
-
\prod_(n ≤ k < m) (f k.+1 / f k) = f m / f n.
+
Lemma telescope_prodf n m (
f :
nat → F) :
+
(∀ k,
n < k < m → f k != 0
) → n < m →
+
\prod_(n ≤ k < m) (f k.+1 / f k) = f m / f n.
Lemma addf_div x1 y1 x2 y2 :
-
y1 != 0
→ y2 != 0
→ x1 / y1 + x2 / y2 = (x1 × y2 + x2 × y1) / (y1 × y2).
+
y1 != 0
→ y2 != 0
→ x1 / y1 + x2 / y2 = (x1 × y2 + x2 × y1) / (y1 × y2).
-
Lemma mulf_div x1 y1 x2 y2 :
(x1 / y1) × (x2 / y2) = (x1 × x2) / (y1 × y2).
+
Lemma mulf_div x1 y1 x2 y2 :
(x1 / y1) × (x2 / y2) = (x1 × x2) / (y1 × y2).
Lemma char0_natf_div :
-
[char F] =i pred0 → ∀ m d,
d %| m → (m %/ d)%:R = m%:R / d%:R :> F.
+
[char F] =i pred0 → ∀ m d,
d %| m → (m %/ d)%:R = m%:R / d%:R :> F.
Section FieldMorphismInj.
-
Variables (
R :
ringType) (
f :
{rmorphism F → R}).
+
Variables (
R :
ringType) (
f :
{rmorphism F → R}).
-
Lemma fmorph_eq0 x :
(f x == 0
) = (x == 0
).
+
Lemma fmorph_eq0 x :
(f x == 0
) = (x == 0
).
-
Lemma fmorph_inj :
injective f.
+
Lemma fmorph_inj :
injective f.
-
Lemma fmorph_eq1 x :
(f x == 1
) = (x == 1
).
+
Lemma fmorph_eq1 x :
(f x == 1
) = (x == 1
).
-
Lemma fmorph_char :
[char R] =i [char F].
+
Lemma fmorph_char :
[char R] =i [char F].
End FieldMorphismInj.
@@ -4772,22 +4793,22 @@
Section FieldMorphismInv.
-
Variables (
R :
unitRingType) (
f :
{rmorphism F → R}).
+
Variables (
R :
unitRingType) (
f :
{rmorphism F → R}).
-
Lemma fmorph_unit x :
(f x \in unit) = (x != 0
).
+
Lemma fmorph_unit x :
(f x \in unit) = (x != 0
).
-
Lemma fmorphV :
{morph f: x / x^-1}.
+
Lemma fmorphV :
{morph f: x / x^-1}.
-
Lemma fmorph_div :
{morph f : x y / x / y}.
+
Lemma fmorph_div :
{morph f : x y / x / y}.
End FieldMorphismInv.
-
Canonical regular_fieldType :=
[fieldType of F^o].
+
Canonical regular_fieldType :=
[fieldType of F^o].
Section ModuleTheory.
@@ -4797,44 +4818,44 @@
Implicit Types (
a :
F) (
v :
V).
-
Lemma scalerK a :
a != 0
→ cancel (
*:%R a : V → V) (
*:%R a^-1).
+
Lemma scalerK a :
a != 0
→ cancel (
*:%R a : V → V) (
*:%R a^-1).
-
Lemma scalerKV a :
a != 0
→ cancel (
*:%R a^-1 : V → V) (
*:%R a).
+
Lemma scalerKV a :
a != 0
→ cancel (
*:%R a^-1 : V → V) (
*:%R a).
-
Lemma scalerI a :
a != 0
→ injective (
*:%R a : V → V).
+
Lemma scalerI a :
a != 0
→ injective (
*:%R a : V → V).
-
Lemma scaler_eq0 a v :
(a *: v == 0
) = (a == 0
) || (v == 0
).
+
Lemma scaler_eq0 a v :
(a *: v == 0
) = (a == 0
) || (v == 0
).
-
Lemma rpredZeq S (
modS :
submodPred S) (
kS :
keyed_pred modS)
a v :
-
(a *: v \in kS) = (a == 0
) || (v \in kS).
+
Lemma rpredZeq S (
modS :
submodPred S) (
kS :
keyed_pred modS)
a v :
+
(a *: v \in kS) = (a == 0
) || (v \in kS).
End ModuleTheory.
-
Lemma char_lalg (
A :
lalgType F) :
[char A] =i [char F].
+
Lemma char_lalg (
A :
lalgType F) :
[char A] =i [char F].
Section Predicates.
-
Context (
S :
pred_class) (
divS : @
divrPred F S) (
kS :
keyed_pred divS).
+
Context (
S :
{pred F}) (
divS : @
divrPred F S) (
kS :
keyed_pred divS).
-
Lemma fpredMl x y :
x \in kS → x != 0
→ (x × y \in kS) = (y \in kS).
+
Lemma fpredMl x y :
x \in kS → x != 0
→ (x × y \in kS) = (y \in kS).
-
Lemma fpredMr x y :
x \in kS → x != 0
→ (y × x \in kS) = (y \in kS).
+
Lemma fpredMr x y :
x \in kS → x != 0
→ (y × x \in kS) = (y \in kS).
-
Lemma fpred_divl x y :
x \in kS → x != 0
→ (x / y \in kS) = (y \in kS).
+
Lemma fpred_divl x y :
x \in kS → x != 0
→ (x / y \in kS) = (y \in kS).
-
Lemma fpred_divr x y :
x \in kS → x != 0
→ (y / x \in kS) = (y \in kS).
+
Lemma fpred_divr x y :
x \in kS → x != 0
→ (y / x \in kS) = (y \in kS).
End Predicates.
@@ -4848,43 +4869,43 @@
Module DecidableField.
-
Definition axiom (
R :
unitRingType) (
s :
seq R → pred (
formula R)) :=
-
∀ e f,
reflect (
holds e f) (
s e f).
+
Definition axiom (
R :
unitRingType) (
s :
seq R → pred (
formula R)) :=
+
∀ e f,
reflect (
holds e f) (
s e f).
Record mixin_of (
R :
unitRingType) :
Type :=
-
Mixin {
sat :
seq R → pred (
formula R);
satP :
axiom sat}.
+
Mixin {
sat :
seq R → pred (
formula R);
satP :
axiom sat}.
Section ClassDef.
Record class_of (
F :
Type) :
Type :=
-
Class {
base :
Field.class_of F;
mixin :
mixin_of (
UnitRing.Pack base F)}.
+
Class {
base :
Field.class_of F;
mixin :
mixin_of (
UnitRing.Pack base)}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variable (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
-
Definition pack b0 (
m0 :
mixin_of (@
UnitRing.Pack T b0 T)) :=
-
fun bT b &
phant_id (
Field.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
Definition pack b0 (
m0 :
mixin_of (@
UnitRing.Pack T b0)) :=
+
fun bT b &
phant_id (
Field.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
IntegralDomain.Pack cT xclass xT.
-
Definition fieldType := @
Field.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
IntegralDomain.Pack cT xclass.
+
Definition fieldType := @
Field.Pack cT xclass.
End ClassDef.
@@ -4913,11 +4934,11 @@
Coercion fieldType : type >-> Field.type.
Canonical fieldType.
Notation decFieldType :=
type.
-
Notation DecFieldType T m := (@
pack T _ m _ _ id _ id).
+
Notation DecFieldType T m := (@
pack T _ m _ _ id _ id).
Notation DecFieldMixin :=
Mixin.
-
Notation "[ 'decFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation "[ 'decFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'decFieldType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'decFieldType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'decFieldType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'decFieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -4939,26 +4960,26 @@
Fact sol_subproof n f :
-
reflect (
∃ s, (size s == n) && sat s f)
- (
sat [::] (
foldr Exists f (
iota 0
n))).
+
reflect (
∃ s, (size s == n) && sat s f)
+ (
sat [::] (
foldr Exists f (
iota 0
n))).
Definition sol n f :=
if sol_subproof n f is ReflectT sP then xchoose sP else nseq n 0.
-
Lemma size_sol n f :
size (
sol n f)
= n.
+
Lemma size_sol n f :
size (
sol n f)
= n.
-
Lemma solP n f :
reflect (
exists2 s, size s = n & holds s f) (
sat (
sol n f)
f).
+
Lemma solP n f :
reflect (
exists2 s, size s = n & holds s f) (
sat (
sol n f)
f).
Lemma eq_sat f1 f2 :
-
(∀ e,
holds e f1 ↔ holds e f2) → sat^~ f1 =1 sat^~ f2.
+
(∀ e,
holds e f1 ↔ holds e f2) → sat^~ f1 =1 sat^~ f2.
Lemma eq_sol f1 f2 :
-
(∀ e,
holds e f1 ↔ holds e f2) → sol^~ f1 =1 sol^~ f2.
+
(∀ e,
holds e f1 ↔ holds e f2) → sol^~ f1 =1 sol^~ f2.
End DecidableFieldTheory.
@@ -4973,7 +4994,7 @@
Implicit Type f :
formula F.
-
Variable proj :
nat → seq (
term F)
× seq (
term F)
→ formula F.
+
Variable proj :
nat → seq (
term F)
× seq (
term F)
→ formula F.
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
IntegralDomain.Pack cT xclass xT.
-
Definition fieldType := @
Field.Pack cT xclass xT.
-
Definition decFieldType := @
DecidableField.Pack cT class xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
IntegralDomain.Pack cT xclass.
+
Definition fieldType := @
Field.Pack cT xclass.
+
Definition decFieldType := @
DecidableField.Pack cT class.
End ClassDef.
@@ -5119,10 +5140,10 @@
Coercion decFieldType : type >-> DecidableField.type.
Canonical decFieldType.
Notation closedFieldType :=
type.
-
Notation ClosedFieldType T m := (@
pack T _ m _ _ id _ id).
-
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation ClosedFieldType T m := (@
pack T _ m _ _ id _ id).
+
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'closedFieldType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'closedFieldType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'closedFieldType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'closedFieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -5140,7 +5161,7 @@
Lemma solve_monicpoly :
ClosedField.axiom F.
-
Lemma imaginary_exists :
{i : F | i ^+ 2
= -1
}.
+
Lemma imaginary_exists :
{i : F | i ^+ 2
= -1
}.
End ClosedFieldTheory.
@@ -5152,9 +5173,9 @@
Section Zmodule.
-
Variables (
V :
zmodType) (
S :
predPredType V).
-
Variables (
subS :
zmodPred S) (
kS :
keyed_pred subS).
-
Variable U :
subType (
mem kS).
+
Variables (
V :
zmodType) (
S :
{pred V}).
+
Variables (
subS :
zmodPred S) (
kS :
keyed_pred subS).
+
Variable U :
subType (
mem kS).
Let inU v Sv :
U :=
Sub v Sv.
@@ -5165,13 +5186,13 @@
Let addU (
u1 u2 :
U) :=
inU (
rpredD (
valP u1) (
valP u2)).
-
Fact addA :
associative addU.
-
Fact addC :
commutative addU.
-
Fact add0 :
left_id zeroU addU.
-
Fact addN :
left_inverse zeroU oppU addU.
+
Fact addA :
associative addU.
+
Fact addC :
commutative addU.
+
Fact add0 :
left_id zeroU addU.
+
Fact addN :
left_inverse zeroU oppU addU.
-
Definition zmodMixin of phant U :=
ZmodMixin addA addC add0 addN.
+
Definition zmodMixin of phant U :=
ZmodMixin addA addC add0 addN.
End Zmodule.
@@ -5180,16 +5201,16 @@
Section Ring.
-
Variables (
R :
ringType) (
S :
predPredType R).
-
Variables (
ringS :
subringPred S) (
kS :
keyed_pred ringS).
+
Variables (
R :
ringType) (
S :
{pred R}).
+
Variables (
ringS :
subringPred S) (
kS :
keyed_pred ringS).
-
Definition cast_zmodType (
V :
zmodType)
T (
VeqT :
V = T :> Type) :=
-
let cast mV :=
let:
erefl in _ = T :=
VeqT return Zmodule.class_of T in mV in
-
Zmodule.Pack (
cast (
Zmodule.class V))
T.
+
Definition cast_zmodType (
V :
zmodType)
T (
VeqT :
V = T :> Type) :=
+
let cast mV :=
let:
erefl in _ = T :=
VeqT return Zmodule.class_of T in mV in
+
Zmodule.Pack (
cast (
Zmodule.class V)).
-
Variable (
T :
subType (
mem kS)) (
V :
zmodType) (
VeqT:
V = T :> Type).
+
Variable (
T :
subType (
mem kS)) (
V :
zmodType) (
VeqT:
V = T :> Type).
Let inT x Sx :
T :=
Sub x Sx.
@@ -5198,19 +5219,19 @@
Let T' :=
cast_zmodType VeqT.
-
Hypothesis valM :
{morph (val : T' → R) : x y / x - y}.
+
Hypothesis valM :
{morph (val : T' → R) : x y / x - y}.
-
Let val0 :
val (0
: T')
= 0.
-
Let valD :
{morph (val : T' → R): x y / x + y}.
+
Let val0 :
val (0
: T')
= 0.
+
Let valD :
{morph (val : T' → R): x y / x + y}.
-
Fact mulA : @
associative T' mulT.
-
Fact mul1l :
left_id oneT mulT.
-
Fact mul1r :
right_id oneT mulT.
-
Fact mulDl : @
left_distributive T' T' mulT +%R.
-
Fact mulDr : @
right_distributive T' T' mulT +%R.
-
Fact nz1 :
oneT != 0
:> T'.
+
Fact mulA : @
associative T' mulT.
+
Fact mul1l :
left_id oneT mulT.
+
Fact mul1r :
right_id oneT mulT.
+
Fact mulDl : @
left_distributive T' T' mulT +%R.
+
Fact mulDr : @
right_distributive T' T' mulT +%R.
+
Fact nz1 :
oneT != 0
:> T'.
Definition ringMixin :=
RingMixin mulA mul1l mul1r mulDl mulDr nz1.
@@ -5222,22 +5243,22 @@
Section Lmodule.
-
Variables (
R :
ringType) (
V :
lmodType R) (
S :
predPredType V).
-
Variables (
linS :
submodPred S) (
kS :
keyed_pred linS).
-
Variables (
W :
subType (
mem kS)) (
Z :
zmodType) (
ZeqW :
Z = W :> Type).
+
Variables (
R :
ringType) (
V :
lmodType R) (
S :
{pred V}).
+
Variables (
linS :
submodPred S) (
kS :
keyed_pred linS).
+
Variables (
W :
subType (
mem kS)) (
Z :
zmodType) (
ZeqW :
Z = W :> Type).
-
Let scaleW a (
w :
W) := (
Sub _ : _ → W) (
rpredZ a (
valP w)).
+
Let scaleW a (
w :
W) := (
Sub _ : _ → W) (
rpredZ a (
valP w)).
Let W' :=
cast_zmodType ZeqW.
-
Hypothesis valD :
{morph (val : W' → V) : x y / x + y}.
+
Hypothesis valD :
{morph (val : W' → V) : x y / x + y}.
-
Fact scaleA a b (
w :
W') :
scaleW a (
scaleW b w)
= scaleW (
a × b)
w.
-
Fact scale1 :
left_id 1
scaleW.
-
Fact scaleDr : @
right_distributive R W' scaleW +%R.
-
Fact scaleDl w :
{morph (scaleW^~ w : R → W') : a b / a + b}.
+
Fact scaleA a b (
w :
W') :
scaleW a (
scaleW b w)
= scaleW (
a × b)
w.
+
Fact scale1 :
left_id 1
scaleW.
+
Fact scaleDr : @
right_distributive R W' scaleW +%R.
+
Fact scaleDl w :
{morph (scaleW^~ w : R → W') : a b / a + b}.
Definition lmodMixin :=
LmodMixin scaleA scale1 scaleDr scaleDl.
@@ -5246,56 +5267,56 @@
End Lmodule.
-
Lemma lalgMixin (
R :
ringType) (
A :
lalgType R) (
B :
lmodType R) (
f :
B → A) :
-
phant B → injective f → scalable f →
-
∀ mulB,
{morph f : x y / mulB x y >-> x × y} → Lalgebra.axiom mulB.
+
Lemma lalgMixin (
R :
ringType) (
A :
lalgType R) (
B :
lmodType R) (
f :
B → A) :
+
phant B → injective f → scalable f →
+
∀ mulB,
{morph f : x y / mulB x y >-> x × y} → Lalgebra.axiom mulB.
-
Lemma comRingMixin (
R :
comRingType) (
T :
ringType) (
f :
T → R) :
-
phant T → injective f → {morph f : x y / x × y} → commutative (@
mul T).
+
Lemma comRingMixin (
R :
comRingType) (
T :
ringType) (
f :
T → R) :
+
phant T → injective f → {morph f : x y / x × y} → commutative (@
mul T).
-
Lemma algMixin (
R :
comRingType) (
A :
algType R) (
B :
lalgType R) (
f :
B → A) :
-
phant B → injective f → {morph f : x y / x × y} → scalable f →
+
Lemma algMixin (
R :
comRingType) (
A :
algType R) (
B :
lalgType R) (
f :
B → A) :
+
phant B → injective f → {morph f : x y / x × y} → scalable f →
@
Algebra.axiom R B.
Section UnitRing.
-
Definition cast_ringType (
Q :
ringType)
T (
QeqT :
Q = T :> Type) :=
-
let cast rQ :=
let:
erefl in _ = T :=
QeqT return Ring.class_of T in rQ in
-
Ring.Pack (
cast (
Ring.class Q))
T.
+
Definition cast_ringType (
Q :
ringType)
T (
QeqT :
Q = T :> Type) :=
+
let cast rQ :=
let:
erefl in _ = T :=
QeqT return Ring.class_of T in rQ in
+
Ring.Pack (
cast (
Ring.class Q)).
-
Variables (
R :
unitRingType) (
S :
predPredType R).
-
Variables (
ringS :
divringPred S) (
kS :
keyed_pred ringS).
+
Variables (
R :
unitRingType) (
S :
{pred R}).
+
Variables (
ringS :
divringPred S) (
kS :
keyed_pred ringS).
-
Variables (
T :
subType (
mem kS)) (
Q :
ringType) (
QeqT :
Q = T :> Type).
+
Variables (
T :
subType (
mem kS)) (
Q :
ringType) (
QeqT :
Q = T :> Type).
Let inT x Sx :
T :=
Sub x Sx.
Let invT (
u :
T) :=
inT (
rpredVr (
valP u)).
-
Let unitT :=
[qualify a u : T | val u \is a unit].
+
Let unitT :=
[qualify a u : T | val u \is a unit].
Let T' :=
cast_ringType QeqT.
-
Hypothesis val1 :
val (1
: T')
= 1.
-
Hypothesis valM :
{morph (val : T' → R) : x y / x × y}.
+
Hypothesis val1 :
val (1
: T')
= 1.
+
Hypothesis valM :
{morph (val : T' → R) : x y / x × y}.
Fact mulVr :
-
{in (unitT : predPredType T'), left_inverse (1
: T')
invT (@
mul T')
}.
+
{in (unitT : {pred T'}), left_inverse (1
: T')
invT (@
mul T')
}.
-
Fact mulrV :
{in unitT, right_inverse (1
: T')
invT (@
mul T')
}.
+
Fact mulrV :
{in unitT, right_inverse (1
: T')
invT (@
mul T')
}.
-
Fact unitP (
u v :
T') :
v × u = 1
∧ u × v = 1
→ u \in unitT.
+
Fact unitP (
u v :
T') :
v × u = 1
∧ u × v = 1
→ u \in unitT.
-
Fact unit_id :
{in [predC unitT], invT =1 id}.
+
Fact unit_id :
{in [predC unitT], invT =1 id}.
Definition unitRingMixin :=
UnitRingMixin mulVr mulrV unitP unit_id.
@@ -5304,44 +5325,44 @@
End UnitRing.
-
Lemma idomainMixin (
R :
idomainType) (
T :
ringType) (
f :
T → R) :
-
phant T → injective f → f 0
= 0
→ {morph f : u v / u × v} →
+
Lemma idomainMixin (
R :
idomainType) (
T :
ringType) (
f :
T → R) :
+
phant T → injective f → f 0
= 0
→ {morph f : u v / u × v} →
@
IntegralDomain.axiom T.
-
Lemma fieldMixin (
F :
fieldType) (
K :
unitRingType) (
f :
K → F) :
-
phant K → injective f → f 0
= 0
→ {mono f : u / u \in unit} →
+
Lemma fieldMixin (
F :
fieldType) (
K :
unitRingType) (
f :
K → F) :
+
phant K → injective f → f 0
= 0
→ {mono f : u / u \in unit} →
@
Field.mixin_of K.
Module Exports.
-
Notation "[ 'zmodMixin' 'of' U 'by' <: ]" := (
zmodMixin (
Phant U))
+
Notation "[ 'zmodMixin' 'of' U 'by' <: ]" := (
zmodMixin (
Phant U))
(
at level 0,
format "[ 'zmodMixin' 'of' U 'by' <: ]") :
form_scope.
-
Notation "[ 'ringMixin' 'of' R 'by' <: ]" :=
- (@
ringMixin _ _ _ _ _ _ (@
erefl Type R%
type) (
rrefl _))
+
Notation "[ 'ringMixin' 'of' R 'by' <: ]" :=
+ (@
ringMixin _ _ _ _ _ _ (@
erefl Type R%
type) (
rrefl _))
(
at level 0,
format "[ 'ringMixin' 'of' R 'by' <: ]") :
form_scope.
-
Notation "[ 'lmodMixin' 'of' U 'by' <: ]" :=
- (@
lmodMixin _ _ _ _ _ _ _ (@
erefl Type U%
type) (
rrefl _))
+
Notation "[ 'lmodMixin' 'of' U 'by' <: ]" :=
+ (@
lmodMixin _ _ _ _ _ _ _ (@
erefl Type U%
type) (
rrefl _))
(
at level 0,
format "[ 'lmodMixin' 'of' U 'by' <: ]") :
form_scope.
-
Notation "[ 'lalgMixin' 'of' A 'by' <: ]" :=
- ((
lalgMixin (
Phant A)
val_inj (
rrefl _))
*%R (
rrefl _))
+
Notation "[ 'lalgMixin' 'of' A 'by' <: ]" :=
+ ((
lalgMixin (
Phant A)
val_inj (
rrefl _))
*%R (
rrefl _))
(
at level 0,
format "[ 'lalgMixin' 'of' A 'by' <: ]") :
form_scope.
-
Notation "[ 'comRingMixin' 'of' R 'by' <: ]" :=
- (
comRingMixin (
Phant R)
val_inj (
rrefl _))
+
Notation "[ 'comRingMixin' 'of' R 'by' <: ]" :=
+ (
comRingMixin (
Phant R)
val_inj (
rrefl _))
(
at level 0,
format "[ 'comRingMixin' 'of' R 'by' <: ]") :
form_scope.
-
Notation "[ 'algMixin' 'of' A 'by' <: ]" :=
- (
algMixin (
Phant A)
val_inj (
rrefl _) (
rrefl _))
+
Notation "[ 'algMixin' 'of' A 'by' <: ]" :=
+ (
algMixin (
Phant A)
val_inj (
rrefl _) (
rrefl _))
(
at level 0,
format "[ 'algMixin' 'of' A 'by' <: ]") :
form_scope.
-
Notation "[ 'unitRingMixin' 'of' R 'by' <: ]" :=
- (@
unitRingMixin _ _ _ _ _ _ (@
erefl Type R%
type) (
erefl _) (
rrefl _))
+
Notation "[ 'unitRingMixin' 'of' R 'by' <: ]" :=
+ (@
unitRingMixin _ _ _ _ _ _ (@
erefl Type R%
type) (
erefl _) (
rrefl _))
(
at level 0,
format "[ 'unitRingMixin' 'of' R 'by' <: ]") :
form_scope.
-
Notation "[ 'idomainMixin' 'of' R 'by' <: ]" :=
- (
idomainMixin (
Phant R)
val_inj (
erefl _) (
rrefl _))
+
Notation "[ 'idomainMixin' 'of' R 'by' <: ]" :=
+ (
idomainMixin (
Phant R)
val_inj (
erefl _) (
rrefl _))
(
at level 0,
format "[ 'idomainMixin' 'of' R 'by' <: ]") :
form_scope.
-
Notation "[ 'fieldMixin' 'of' F 'by' <: ]" :=
- (
fieldMixin (
Phant F)
val_inj (
erefl _) (
frefl _))
+
Notation "[ 'fieldMixin' 'of' F 'by' <: ]" :=
+ (
fieldMixin (
Phant F)
val_inj (
erefl _) (
frefl _))
(
at level 0,
format "[ 'fieldMixin' 'of' F 'by' <: ]") :
form_scope.
@@ -5374,12 +5395,14 @@
Definition addIr := @
addIr.
Definition subrI := @
subrI.
Definition subIr := @
subIr.
-
Definition opprK :=
opprK.
+
Definition opprK := @
opprK.
Definition oppr_inj := @
oppr_inj.
Definition oppr0 :=
oppr0.
Definition oppr_eq0 :=
oppr_eq0.
Definition opprD :=
opprD.
Definition opprB :=
opprB.
+
Definition addrKA :=
addrKA.
+
Definition subrKA :=
subrKA.
Definition subr0 :=
subr0.
Definition sub0r :=
sub0r.
Definition subr_eq :=
subr_eq.
@@ -5557,7 +5580,7 @@
Definition telescope_prodr :=
telescope_prodr.
Definition commrV :=
commrV.
Definition unitrE :=
unitrE.
-
Definition invrK :=
invrK.
+
Definition invrK := @
invrK.
Definition invr_inj := @
invr_inj.
Definition unitrV :=
unitrV.
Definition unitr1 :=
unitr1.
@@ -5808,94 +5831,94 @@
Notation QEdecFieldMixin :=
QEdecFieldMixin.
-
Notation "0" := (
zero _) :
ring_scope.
-
Notation "-%R" := (@
opp _) :
ring_scope.
-
Notation "- x" := (
opp x) :
ring_scope.
-
Notation "+%R" := (@
add _).
-
Notation "x + y" := (
add x y) :
ring_scope.
-
Notation "x - y" := (
add x (
- y)) :
ring_scope.
-
Notation "x *+ n" := (
natmul x n) :
ring_scope.
-
Notation "x *- n" := (
opp (
x *+ n)) :
ring_scope.
-
Notation "s `_ i" := (
seq.nth 0%
R s%
R i) :
ring_scope.
-
Notation support := 0
.-support.
+
Notation "0" := (
zero _) :
ring_scope.
+
Notation "-%R" := (@
opp _) :
ring_scope.
+
Notation "- x" := (
opp x) :
ring_scope.
+
Notation "+%R" := (@
add _).
+
Notation "x + y" := (
add x y) :
ring_scope.
+
Notation "x - y" := (
add x (
- y)) :
ring_scope.
+
Notation "x *+ n" := (
natmul x n) :
ring_scope.
+
Notation "x *- n" := (
opp (
x *+ n)) :
ring_scope.
+
Notation "s `_ i" := (
seq.nth 0%
R s%
R i) :
ring_scope.
+
Notation support := 0
.-support.
-
Notation "1" := (
one _) :
ring_scope.
-
Notation "- 1" := (
opp 1) :
ring_scope.
+
Notation "1" := (
one _) :
ring_scope.
+
Notation "- 1" := (
opp 1) :
ring_scope.
-
Notation "n %:R" := (
natmul 1
n) :
ring_scope.
-
Notation "[ 'char' R ]" := (
char (
Phant R)) :
ring_scope.
+
Notation "n %:R" := (
natmul 1
n) :
ring_scope.
+
Notation "[ 'char' R ]" := (
char (
Phant R)) :
ring_scope.
Notation Frobenius_aut chRp := (
Frobenius_aut chRp).
-
Notation "*%R" := (@
mul _).
-
Notation "x * y" := (
mul x y) :
ring_scope.
-
Notation "x ^+ n" := (
exp x n) :
ring_scope.
-
Notation "x ^-1" := (
inv x) :
ring_scope.
-
Notation "x ^- n" := (
inv (
x ^+ n)) :
ring_scope.
-
Notation "x / y" := (
mul x y^-1) :
ring_scope.
-
-
-
Notation "*:%R" := (@
scale _ _).
-
Notation "a *: m" := (
scale a m) :
ring_scope.
-
Notation "k %:A" := (
scale k 1) :
ring_scope.
-
Notation "\0" := (
null_fun _) :
ring_scope.
-
Notation "f \+ g" := (
add_fun_head tt f g) :
ring_scope.
-
Notation "f \- g" := (
sub_fun_head tt f g) :
ring_scope.
-
Notation "a \*: f" := (
scale_fun_head tt a f) :
ring_scope.
-
Notation "x \*o f" := (
mull_fun_head tt x f) :
ring_scope.
-
Notation "x \o* f" := (
mulr_fun_head tt x f) :
ring_scope.
-
-
-
Notation "\sum_ ( i <- r | P ) F" :=
- (
\big[+%R/0%
R]_(i <- r | P%
B) F%
R) :
ring_scope.
-
Notation "\sum_ ( i <- r ) F" :=
- (
\big[+%R/0%
R]_(i <- r) F%
R) :
ring_scope.
-
Notation "\sum_ ( m <= i < n | P ) F" :=
- (
\big[+%R/0%
R]_(m ≤ i < n | P%
B) F%
R) :
ring_scope.
-
Notation "\sum_ ( m <= i < n ) F" :=
- (
\big[+%R/0%
R]_(m ≤ i < n) F%
R) :
ring_scope.
-
Notation "\sum_ ( i | P ) F" :=
- (
\big[+%R/0%
R]_(i | P%
B) F%
R) :
ring_scope.
-
Notation "\sum_ i F" :=
- (
\big[+%R/0%
R]_i F%
R) :
ring_scope.
-
Notation "\sum_ ( i : t | P ) F" :=
- (
\big[+%R/0%
R]_(i : t | P%
B) F%
R) (
only parsing) :
ring_scope.
-
Notation "\sum_ ( i : t ) F" :=
- (
\big[+%R/0%
R]_(i : t) F%
R) (
only parsing) :
ring_scope.
-
Notation "\sum_ ( i < n | P ) F" :=
- (
\big[+%R/0%
R]_(i < n | P%
B) F%
R) :
ring_scope.
-
Notation "\sum_ ( i < n ) F" :=
- (
\big[+%R/0%
R]_(i < n) F%
R) :
ring_scope.
-
Notation "\sum_ ( i 'in' A | P ) F" :=
- (
\big[+%R/0%
R]_(i in A | P%
B) F%
R) :
ring_scope.
-
Notation "\sum_ ( i 'in' A ) F" :=
- (
\big[+%R/0%
R]_(i in A) F%
R) :
ring_scope.
-
-
-
Notation "\prod_ ( i <- r | P ) F" :=
- (
\big[*%R/1%
R]_(i <- r | P%
B) F%
R) :
ring_scope.
-
Notation "\prod_ ( i <- r ) F" :=
- (
\big[*%R/1%
R]_(i <- r) F%
R) :
ring_scope.
-
Notation "\prod_ ( m <= i < n | P ) F" :=
- (
\big[*%R/1%
R]_(m ≤ i < n | P%
B) F%
R) :
ring_scope.
-
Notation "\prod_ ( m <= i < n ) F" :=
- (
\big[*%R/1%
R]_(m ≤ i < n) F%
R) :
ring_scope.
-
Notation "\prod_ ( i | P ) F" :=
- (
\big[*%R/1%
R]_(i | P%
B) F%
R) :
ring_scope.
-
Notation "\prod_ i F" :=
- (
\big[*%R/1%
R]_i F%
R) :
ring_scope.
-
Notation "\prod_ ( i : t | P ) F" :=
- (
\big[*%R/1%
R]_(i : t | P%
B) F%
R) (
only parsing) :
ring_scope.
-
Notation "\prod_ ( i : t ) F" :=
- (
\big[*%R/1%
R]_(i : t) F%
R) (
only parsing) :
ring_scope.
-
Notation "\prod_ ( i < n | P ) F" :=
- (
\big[*%R/1%
R]_(i < n | P%
B) F%
R) :
ring_scope.
-
Notation "\prod_ ( i < n ) F" :=
- (
\big[*%R/1%
R]_(i < n) F%
R) :
ring_scope.
-
Notation "\prod_ ( i 'in' A | P ) F" :=
- (
\big[*%R/1%
R]_(i in A | P%
B) F%
R) :
ring_scope.
-
Notation "\prod_ ( i 'in' A ) F" :=
- (
\big[*%R/1%
R]_(i in A) F%
R) :
ring_scope.
+
Notation "*%R" := (@
mul _).
+
Notation "x * y" := (
mul x y) :
ring_scope.
+
Notation "x ^+ n" := (
exp x n) :
ring_scope.
+
Notation "x ^-1" := (
inv x) :
ring_scope.
+
Notation "x ^- n" := (
inv (
x ^+ n)) :
ring_scope.
+
Notation "x / y" := (
mul x y^-1) :
ring_scope.
+
+
+
Notation "*:%R" := (@
scale _ _).
+
Notation "a *: m" := (
scale a m) :
ring_scope.
+
Notation "k %:A" := (
scale k 1) :
ring_scope.
+
Notation "\0" := (
null_fun _) :
ring_scope.
+
Notation "f \+ g" := (
add_fun_head tt f g) :
ring_scope.
+
Notation "f \- g" := (
sub_fun_head tt f g) :
ring_scope.
+
Notation "a \*: f" := (
scale_fun_head tt a f) :
ring_scope.
+
Notation "x \*o f" := (
mull_fun_head tt x f) :
ring_scope.
+
Notation "x \o* f" := (
mulr_fun_head tt x f) :
ring_scope.
+
+
+
Notation "\sum_ ( i <- r | P ) F" :=
+ (
\big[+%R/0%
R]_(i <- r | P%
B) F%
R) :
ring_scope.
+
Notation "\sum_ ( i <- r ) F" :=
+ (
\big[+%R/0%
R]_(i <- r) F%
R) :
ring_scope.
+
Notation "\sum_ ( m <= i < n | P ) F" :=
+ (
\big[+%R/0%
R]_(m ≤ i < n | P%
B) F%
R) :
ring_scope.
+
Notation "\sum_ ( m <= i < n ) F" :=
+ (
\big[+%R/0%
R]_(m ≤ i < n) F%
R) :
ring_scope.
+
Notation "\sum_ ( i | P ) F" :=
+ (
\big[+%R/0%
R]_(i | P%
B) F%
R) :
ring_scope.
+
Notation "\sum_ i F" :=
+ (
\big[+%R/0%
R]_i F%
R) :
ring_scope.
+
Notation "\sum_ ( i : t | P ) F" :=
+ (
\big[+%R/0%
R]_(i : t | P%
B) F%
R) (
only parsing) :
ring_scope.
+
Notation "\sum_ ( i : t ) F" :=
+ (
\big[+%R/0%
R]_(i : t) F%
R) (
only parsing) :
ring_scope.
+
Notation "\sum_ ( i < n | P ) F" :=
+ (
\big[+%R/0%
R]_(i < n | P%
B) F%
R) :
ring_scope.
+
Notation "\sum_ ( i < n ) F" :=
+ (
\big[+%R/0%
R]_(i < n) F%
R) :
ring_scope.
+
Notation "\sum_ ( i 'in' A | P ) F" :=
+ (
\big[+%R/0%
R]_(i in A | P%
B) F%
R) :
ring_scope.
+
Notation "\sum_ ( i 'in' A ) F" :=
+ (
\big[+%R/0%
R]_(i in A) F%
R) :
ring_scope.
+
+
+
Notation "\prod_ ( i <- r | P ) F" :=
+ (
\big[*%R/1%
R]_(i <- r | P%
B) F%
R) :
ring_scope.
+
Notation "\prod_ ( i <- r ) F" :=
+ (
\big[*%R/1%
R]_(i <- r) F%
R) :
ring_scope.
+
Notation "\prod_ ( m <= i < n | P ) F" :=
+ (
\big[*%R/1%
R]_(m ≤ i < n | P%
B) F%
R) :
ring_scope.
+
Notation "\prod_ ( m <= i < n ) F" :=
+ (
\big[*%R/1%
R]_(m ≤ i < n) F%
R) :
ring_scope.
+
Notation "\prod_ ( i | P ) F" :=
+ (
\big[*%R/1%
R]_(i | P%
B) F%
R) :
ring_scope.
+
Notation "\prod_ i F" :=
+ (
\big[*%R/1%
R]_i F%
R) :
ring_scope.
+
Notation "\prod_ ( i : t | P ) F" :=
+ (
\big[*%R/1%
R]_(i : t | P%
B) F%
R) (
only parsing) :
ring_scope.
+
Notation "\prod_ ( i : t ) F" :=
+ (
\big[*%R/1%
R]_(i : t) F%
R) (
only parsing) :
ring_scope.
+
Notation "\prod_ ( i < n | P ) F" :=
+ (
\big[*%R/1%
R]_(i < n | P%
B) F%
R) :
ring_scope.
+
Notation "\prod_ ( i < n ) F" :=
+ (
\big[*%R/1%
R]_(i < n) F%
R) :
ring_scope.
+
Notation "\prod_ ( i 'in' A | P ) F" :=
+ (
\big[*%R/1%
R]_(i in A | P%
B) F%
R) :
ring_scope.
+
Notation "\prod_ ( i 'in' A ) F" :=
+ (
\big[*%R/1%
R]_(i in A) F%
R) :
ring_scope.
Canonical add_monoid.
@@ -5940,7 +5963,7 @@
Canonical in_alg_rmorphism.
-
Notation "R ^c" := (
converse R) (
at level 2,
format "R ^c") :
type_scope.
+
Notation "R ^c" := (
converse R) (
at level 2,
format "R ^c") :
type_scope.
Canonical converse_eqType.
Canonical converse_choiceType.
Canonical converse_zmodType.
@@ -5948,7 +5971,7 @@
Canonical converse_unitRingType.
-
Notation "R ^o" := (
regular R) (
at level 2,
format "R ^o") :
type_scope.
+
Notation "R ^o" := (
regular R) (
at level 2,
format "R ^o") :
type_scope.
Canonical regular_eqType.
Canonical regular_choiceType.
Canonical regular_zmodType.
@@ -5974,27 +5997,27 @@
-
Notation "''X_' i" := (
Var _ i) :
term_scope.
-
Notation "n %:R" := (
NatConst _ n) :
term_scope.
-
Notation "0" := 0
%:R%
T :
term_scope.
-
Notation "1" := 1
%:R%
T :
term_scope.
-
Notation "x %:T" := (
Const x) :
term_scope.
-
Infix "+" :=
Add :
term_scope.
-
Notation "- t" := (
Opp t) :
term_scope.
-
Notation "t - u" := (
Add t (
- u)) :
term_scope.
-
Infix "×" :=
Mul :
term_scope.
-
Infix "*+" :=
NatMul :
term_scope.
-
Notation "t ^-1" := (
Inv t) :
term_scope.
-
Notation "t / u" := (
Mul t u^-1) :
term_scope.
-
Infix "^+" :=
Exp :
term_scope.
-
Infix "==" :=
Equal :
term_scope.
-
Notation "x != y" := (
GRing.Not (
x == y)) :
term_scope.
-
Infix "∧" :=
And :
term_scope.
-
Infix "∨" :=
Or :
term_scope.
-
Infix "==>" :=
Implies :
term_scope.
-
Notation "~ f" := (
Not f) :
term_scope.
-
Notation "''exists' ''X_' i , f" := (
Exists i f) :
term_scope.
-
Notation "''forall' ''X_' i , f" := (
Forall i f) :
term_scope.
+
Notation "''X_' i" := (
Var _ i) :
term_scope.
+
Notation "n %:R" := (
NatConst _ n) :
term_scope.
+
Notation "0" := 0
%:R%
T :
term_scope.
+
Notation "1" := 1
%:R%
T :
term_scope.
+
Notation "x %:T" := (
Const x) :
term_scope.
+
Infix "+" :=
Add :
term_scope.
+
Notation "- t" := (
Opp t) :
term_scope.
+
Notation "t - u" := (
Add t (
- u)) :
term_scope.
+
Infix "×" :=
Mul :
term_scope.
+
Infix "*+" :=
NatMul :
term_scope.
+
Notation "t ^-1" := (
Inv t) :
term_scope.
+
Notation "t / u" := (
Mul t u^-1) :
term_scope.
+
Infix "^+" :=
Exp :
term_scope.
+
Infix "==" :=
Equal :
term_scope.
+
Notation "x != y" := (
GRing.Not (
x == y)) :
term_scope.
+
Infix "∧" :=
And :
term_scope.
+
Infix "∨" :=
Or :
term_scope.
+
Infix "==>" :=
Implies :
term_scope.
+
Notation "~ f" := (
Not f) :
term_scope.
+
Notation "''exists' ''X_' i , f" := (
Exists i f) :
term_scope.
+
Notation "''forall' ''X_' i , f" := (
Forall i f) :
term_scope.
@@ -6007,18 +6030,18 @@