1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
From mathcomp Require Import all_boot all_order all_algebra all_field.
Section regular.
Import GRing.
Goal forall R : ringType, [the lalgType R of R^o] = R :> ringType.
Proof. by move=> [? []]. Qed.
Goal forall R : comRingType, [the algType R of R^o] = R :> ringType.
Proof. by move=> [? []]. Qed.
Goal forall R : comRingType, [the comAlgType R of R^o] = R :> ringType.
Proof. by move=> [? []]. Qed.
Goal forall R : comUnitRingType, [the unitAlgType R of R^o] = R :> unitRingType.
Proof. by move=> [? []]. Qed.
Goal forall R : comUnitRingType,
[the comUnitAlgType R of R^o] = R :> comUnitRingType.
Proof. by move=> [? []]. Qed.
Goal forall R : comUnitRingType, [the falgType R of R^o] = R :> unitRingType.
Proof. by move=> [? []]. Qed.
Goal forall K : fieldType, [the fieldExtType K of K^o] = K :> fieldType.
Proof. by move=> [? []]. Qed.
End regular.
|
