Skip to the content.
← Ch. 6: Groups Table of contents Ch. 8: Rings →

This chapter proves theorems about an arbitrary group. We are given some Grp : Group G for an unknown G, and we use only the fields from Chapter 6. The point of this chapter lies less in the three theorems themselves (they are standard) than in the search process for finding each proof: given a goal, what to examine, what to attempt, and how to recognize being stuck versus one step away. Each theorem below is presented as that search, not merely its answer.

Learning objectives. By the end of this chapter, prove a fact about every group at once by reasoning only from Group’s fields, recognize the “relate both sides to a common third expression” and “pad with the identity, then cancel” patterns, and reuse a proved lemma (left_inverse_unique) to shortcut a later one (inv_op) instead of re-deriving it.

Sections

  1. Setup
  2. Theorem 1: the identity is unique
  3. Theorem 2: left inverses equal right inverses
  4. Theorem 3: inverse of a product
  5. Exercises

← Ch. 6: Groups Table of contents Ch. 8: Rings →
Try Lean
Lean playground · v1.4.18