.. _groups_and_ring: Grup dan Gelanggang =================== Dalam :numref:`proving_identities_in_algebraic_structures`, kita telah melihat cara menalar tentang operasi pada grup dan gelanggang. Kemudian, dalam :numref:`section_algebraic_structures`, kita melihat cara mendefinisikan struktur aljabar abstrak, seperti struktur grup, beserta instans konkret seperti struktur gelanggang pada bilangan bulat Gauss. :numref:`Bab %s ` menjelaskan cara hierarki struktur abstrak ditangani dalam Mathlib. Dalam bab ini, kita akan mempelajari grup dan gelanggang secara lebih terperinci. Kita tidak akan dapat membahas setiap aspek penanganan topik-topik tersebut dalam Mathlib, terlebih karena Mathlib terus berkembang. Namun, kita akan menyediakan titik masuk ke pustaka dan menunjukkan cara menggunakan konsep-konsep esensial. Ada sedikit tumpang tindih dengan pembahasan dalam :numref:`Bab %s `, tetapi di sini kita akan berfokus pada cara menggunakan Mathlib, bukan pada keputusan desain yang mendasari penanganan topik-topik tersebut. Karena itu, memahami sebagian contoh mungkin memerlukan peninjauan kembali latar belakang dari :numref:`Bab %s `. .. include:: C09_Groups_and_Rings/S01_Groups.inc .. include:: C09_Groups_and_Rings/S02_Rings.inc