Skip to content

Commit

Permalink
cleanup for section on Groups
Browse files Browse the repository at this point in the history
  • Loading branch information
avigad committed Oct 21, 2023
1 parent c98fae1 commit 60dca33
Show file tree
Hide file tree
Showing 2 changed files with 227 additions and 267 deletions.
22 changes: 12 additions & 10 deletions MIL/C08_Groups_and_Rings/C08_Groups_and_Rings.rst
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,17 @@
Groups and rings
================

We saw in :numref:`proving_identities_in_algebraic_structures` how to prove and use lemmas about
operations in groups and ring. Later in :numref:`section_algebraic_structures` we saw how
We saw in :numref:`proving_identities_in_algebraic_structures` how to reason about
operations in groups and rings. Later, in :numref:`section_algebraic_structures`, we saw how
to define abstract algebraic structures, such as group structures, as well as concrete instances
such as the ring structure on Gaussian integers. Then in Chapter :numref:`hierarchies`
we saw how hierarchies of abstract structures are built.
such as the ring structure on the Gaussian integers. :numref:`Chapter %s <hierarchies>` explained how
hierarchies of abstract structures are handled in Mathlib.

In this chapter we will explain a lot more about groups and rings in Mathlib. We won't be able to
cover everything, especially since Mathlib constantly grows. But we will try to provide entry points
and show how essential concepts appear. There is some overlap with the discussion of Chapter
:numref:`hierarchies` but here we will emphasize how to use Mathlib instead of why Mathlib is
built that way. If anything looks strange or convoluted then the explanation is probably
in the previous chapter.
In this chapter we work with groups and rings in more detail. We won't be able to
cover every aspect of the treatement of these topics in Mathlib, especially since Mathlib is constantly growing.
But we will provide entry points to the library and show how the essential concepts are used.
There is some overlap with the discussion of
:numref:`Chapter %s <hierarchies>`, but here we will focus on how to use Mathlib instead of the design
decisions behind the way the topics are treated.
So making sense of some of the examples may require reviewing the background from
:numref:`Chapter %s <hierarchies>`.
Loading

0 comments on commit 60dca33

Please sign in to comment.