README.md

Algebra

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@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, NASA, USA
• André Luiz Galdino, 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, University of Brasília, Brazil
• César Muñoz, NASA, USA
• Mariano Moscato, NIA & NASA, USA
• Sam Owre, SRI, USA

Maintainer

• César Muñoz, NASA, USA

Dependencies