Commit 2019-06-11 04:39 abfaf8d7
View on Github →refactor(group_theory/abelianization): simplify abelianization (#1126)
- 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
- refactor(group_theory/abelianization): simplify abelianization
The commutator of a group was previously defined using lists.
Now it is defined using
normal_closure. This change simplifies some of the proofs