Commit 2019-06-10 13:38 bd2f35f3
View on Github →feat(group_theory/presented_group): define presented groups (#1118)
- feat(group_theory/conjugates) : define conjugates define group conjugates and normal closure
- feat(algebra/order_functions): generalize strict_mono.monotone (#1022)
- trying to merge
- feat(group_theory\presented_group): define presented groups Presented groups are defined as a quotient of a free group by the normal subgroup the relations generate.
- feat(group_theory\presented_group): define presented groups Presented groups are defined as a quotient of a free group by the normal subgroup the relations generate
- Update src/group_theory/presented_group.lean Co-Authored-By: Keeley Hoek keeley@hoek.io
- Uniqueness of extension
- Tidied up to_group.unique
- Removed unnecessary line
- Changed naming