Commit 2021-02-13 22:35 b0aae273

View on Github →

feat(algebra/category/Group/adjunctions): free_group-forgetful adjunction (#6190) Furthermore, a module doc for group_theory/free_group is provided and a few lines in this file are split.

Estimated changes

Modified src/algebra/category/Group/adjunctions.lean

added def Group.adj

added def Group.free

Modified src/group_theory/free_group.lean

modified def free_group.free_group_unit_equiv_int

added def free_group.lift

modified theorem free_group.mul_bind

modified theorem free_group.reduce.not