Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes