.. _structures:

Struktur
========

Matematika modern menggunakan struktur aljabar secara mendasar.
Struktur-struktur ini merangkum pola yang dapat diwujudkan dalam
berbagai latar.
Teori struktur aljabar menyediakan berbagai cara untuk mendefinisikan
struktur semacam itu dan membangun instans tertentu.

Karena itu, Lean menyediakan cara-cara yang bersesuaian untuk
mendefinisikan struktur secara formal dan bekerja dengannya.
Anda telah melihat contoh struktur aljabar dalam Lean, seperti gelanggang
dan kisi, yang dibahas dalam :numref:`Bab %s <basics>`.
Bab ini akan menjelaskan anotasi kurung siku yang tampak misterius
dan telah Anda jumpai di sana, yaitu ``[Ring α]`` dan ``[Lattice α]``.
Bab ini juga akan menunjukkan cara mendefinisikan dan menggunakan
struktur aljabar sendiri.

Untuk uraian yang lebih teknis, Anda dapat membaca
`Theorem Proving in Lean <https://leanprover.github.io/theorem_proving_in_lean/>`_
dan makalah Anne Baanen,
`Use and abuse of instance parameters in the Lean mathematical library <https://arxiv.org/abs/2202.01629>`_.

.. include:: C07_Structures/S01_Structures.inc
.. include:: C07_Structures/S02_Algebraic_Structures.inc
.. include:: C07_Structures/S03_Building_the_Gaussian_Integers.inc