.. _structures:

구조체
======

현대 수학은 여러 환경에서 인스턴스화될 수 있는 패턴을 캡슐화하는 대수적 구조체를 필수적으로 활용합니다. 이 주제는 그러한 구조체를 정의하고 특정 인스턴스를 구성하는 다양한 방법을 제공합니다.

따라서 Lean은 구조체를 형식적으로 정의하고 그것들을 다루는 대응되는 방법을 제공합니다. 여러분은 :numref:`Chapter %s <basics>`\ 에서 다루었던 환이나 격자와 같은 Lean의 대수적 구조체의 예를 이미 살펴보았습니다. 이 장에서는 여러분이 그곳에서 보았던 신비로운 대괄호 표기, 즉 ``[Ring α]``\ 와 ``[Lattice α]``\ 를 설명할 것입니다. 또한 대수적 구조체를 스스로 정의하고 사용하는 방법도 보여줄 것입니다.

더 자세한 기술적인 내용은 `Theorem Proving in Lean <https://lean-lang.org/theorem_proving_in_lean4/>`_\ 와 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