Commit 2023-02-02 13:02 19312750

View on Github →

feat: port GroupTheory.PresentedGroup (#2010)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/PresentedGroup.lean

added theorem PresentedGroup.closure_rels_subset_ker

added def PresentedGroup.of

added theorem PresentedGroup.toGroup.of

added theorem PresentedGroup.toGroup.unique

added def PresentedGroup.toGroup

added theorem PresentedGroup.to_group_eq_one_of_mem_closure

added def PresentedGroup