Merge groups into algebra library (thanks to Andre L. Galdino, Andreia Borges Avelar, Thaynara de Lima, André Camapum Carvalho de Freitas, and Mauricio Ayala-Rincon)

Author: marianomoscato

algebra/CHANGELOG

@@ -1,6 +1,12 @@
-aa940bf	Cesar Munoz	2020-04-02	Removed *.dep
-675d19d	C. Munoz	2020-03-02	Fixed algebra
+        Mariano Moscato	2020-10-09	Merge algebra and groups libraries (thanks to Andre L. Galdino, Andreia Borges Avelar, Thaynara de Lima, André Camapum Carvalho de Freitas, and Mauricio Ayala-Rincon - University of Brasilia)
+30786d3	Mariano Moscato	2020-04-27	Fix proofs for pvs 7.1 version
+12a7ea5	Mariano Moscato	2020-04-20	Cleanup libraries (upgrade proven conjectures to lemmas, remove comments)
+aa940bf	Cesar A. Munoz	2020-04-02	Removed *.dep
+11d2a6d	Mariano Moscato	2020-03-27	Add ring formalization (thanks to Andre L. Galdino, Andreia Borges Avelar, Thaynara de Lima, and Mauricio Ayala-Rincon - University of Brasilia)
+675d19d	Cesar A. Munoz	2020-03-02	Fixed algebra
+0ee39e8	Mariano Moscato	2020-02-28	Fix groups library
 212f3dd	Mariano Moscato	2020-02-14	Apply autofix to fix/clean proofs.
-aa3b091	C. Munoz	2019-05-17	Added summaries and .dep
-9776c00	Sam Owre	2019-02-22	Removed top.dep files
-bb963a7	Sam Owre	2019-02-19	Changes for PVS 7.0
+c51f75e	Mariano Moscato	2019-06-26	Fix proofs in groups (provided by Andre Luiz Galdino, UFB, Brazil)
+aa3b091	Cesar A. Munoz	2019-05-17	Added summaries and .dep
+9776c00	Sam Owre        2019-02-22	Removed top.dep files
+bb963a7	Sam Owre        2019-02-19	Changes for PVS 7.0

algebra/README.md

@@ -4,18 +4,63 @@ Group-, Ring-, and Field-like Mathematical Structures.
 
 ## Highlights
 
+Main contributions:
+  - Cauchy Theorem;
+  - Isomorphism Theorems for Groups;
+  - Burside Theorem;
+  - Sylow Theorems;
+  - Lagrange Theorem;
+  - Fundamental principle of counting;
+  - Formula for permutation with repetition;
+  - Group Action, stabilizer, orbit, normalizer, centralizer, index of a subgroup in a group, and properties;
+  - Class Equation;
+  - P-groups and properties;
+  - Product of Subgroups;
+  - Zn Group, Left and Right Cosets, Factor Group and properties;
+  - Binomial Theorem for Rings; 
+  - Isomorphism Theorems for Rings;
+  - Principal, maximal and prime ideals and properties; 
+  - Quotient rings and properties;
+  - Boolean ring and properties; 
+  - Chinese Remainder Theorem for Rings;
+  - Chinese Remainder Theorem for the Ring of integers.
+  
+
 ### Major theorems
 
 | Theorem | Location | PVS Name | Contributors |
 | --- | --- | --- | --- |
-| Order of a Subgroup | `algebra@finite_group` | `lagrange` | David Lester |
-
+| Order of a Subgroup | `algebra@lagrange` | `Lagrange` | David Lester |
+| First Isomorphism Theorem for Groups | `algebra@homomorphism_lemmas` | `first_isomorphism_th` | André Galdino |
+| Second Isomorphism Theorem for Groups | `algebra@isomorphism_theorems` | `second_isomorphism_th` | André Galdino |
+| Third Isomorphism Theorem for Groups | `algebra@isomorphism_theorems` | `third_isomorphism_th` | André Galdino |
+| Correspondence Theorem for Groups | `algebra@isomorphism_theorems` | `correspondence_theorem` | André Galdino |
+| Cauchy's Theorem for Finite Groups | `algebra@cauchy` | `cauchy` | André Galdino |
+| Burnside's Theorem for p-Groups | `algebra@p_groups` | `burside_theorem` | André Galdino |
+| First Sylow Theorem | `algebra@sylow_theorems` | `First_Sylow_Theorem` | André Galdino |
+| Second Sylow Theorem | `algebra@sylow_theorems` | `Second_Sylow_Theorem` | André Galdino |
+| Third Sylow Theorem | `algebra@sylow_theorems` | `Third_Sylow_Theorem` | André Galdino |
+| Binomial Theorem for Rings| `algebra@ring_binomial_theorem` | `R_bino_theo` | Andréia Avelar, Thaynara de Lima, André Galdino and Mauricio Ayala-Rincón| 
+| Finite integral domains are fields| `algebra@finite_integral_domain` | `fin_int_domain_is_field` | Thaynara de Lima, Andréia Avelar, André Galdino and Mauricio Ayala-Rincón| 
+| First Isomorphism Theorem for Rings| `algebra@ring_1st_isomorphism_theorem` | `first_isomorphism_th` | Andréia Avelar, Thaynara de Lima, André Galdino and Mauricio Ayala-Rincón| 
+| Second Isomorphism Theorem for Rings| `algebra@ring_2nd_3rd_isomorphism_theorems` | `second_isomorphism_th` | Andréia Avelar, Thaynara de Lima, André Galdino and Mauricio Ayala-Rincón| 
+| Third Isomorphism Theorem for Rings| `algebra@ring_2nd_3rd_isomorphism_theorems` | `third_isomorphism_th` | Andréia Avelar, Thaynara de Lima, André Galdino and Mauricio Ayala-Rincón| 
+| Prime Ideals in Commutative Rings| `algebra@ring_with_one_prime_ideal` | `prime_ideal_charac` | Thaynara de Lima, Andréia Avelar, André Galdino and Mauricio Ayala-Rincón|
+| Alternative characterization of principal ideals| `algebra@ring_principal_ideal` | `principal_ideal_charac`| Thaynara de Lima, Andréia Avelar, André Galdino and Mauricio Ayala-Rincón|  
+| Maximal ideals in Commutative Rings| `algebra@ring_with_one_maximal_ideal` | `maximal_ideal_charac`| Thaynara de Lima, Andréia Avelar, André Galdino and Mauricio Ayala-Rincón|  
+| Chinese Remainder Theorem for Rings| `algebra@chinese_remainder_theorem_rings` | `Chinese_Remainder_Theorem` | André Galdino, Thaynara de Lima, Andréia Avelar, and Mauricio Ayala-Rincón|
+| Chinese Remainder Theorem for the Ring Z|`algebra@chinese_remainder_theorem_Z` | `Chinese_Remainder_Theorem_for_int` | André Galdino, Thaynara de Lima, Andréia Avelar, and Mauricio Ayala-Rincón|
 # Contributors
 * David Lester, Manchester University, UK & NIA, USA
 * [Ricky Butler](https://shemesh.larc.nasa.gov/people/rwb/), NASA, USA
+* [André Luiz Galdino](https://galdino.catalao.ufg.br), Federal University of Catalão, Brazil
+* Andréia Borges Avelar, University of Brasília, Brazil
+* Thaynara Arielly de Lima, Federal University of Goiás, Brazil
+* André Camapum Carvalho de Freitas, Federal University of Goiás, Brazil
+* [Mauricio Ayala-Rincón](http://www.mat.unb.br/~ayala), University of Brasília, Brazil
 * [César Muñoz](http://shemesh.larc.nasa.gov/people/cam), NASA, USA
-* [Sam Owre](http://www.csl.sri.com/users/owre), SRI, USA
 * [Mariano Moscato](https://www.nianet.org/directory/research-staff/mariano-moscato/), NIA & NASA, USA
+* [Sam Owre](http://www.csl.sri.com/users/owre), SRI, USA
 
 ## Maintainer
 * [César Muñoz](http://shemesh.larc.nasa.gov/people/cam), NASA, USA