mathlib3
chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum
#1604
Merged
Overview
Commits
4
Changes
View On GitHub

chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum #1604

mergify merged 4 commits into master from lint_mathlib
robertylewis
robertylewis chore(order/zorn): rename zorn.zorn
020007ec
robertylewis chore(group_theory/free_group): rename sum.sum
d7101ece
robertylewis chore(group_theory/free_group,order/zorn): remove nolint
f16c03e6
robertylewis robertylewis changed the title hore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum 6 years ago
kim-em
kim-em approved these changes on 2019-10-24
jcommelin
jcommelin approved these changes on 2019-10-24
jcommelin jcommelin added ready-to-merge
mergify[bot] Merge branch 'master' into lint_mathlib
d0286a80
mergify mergify merged b1f44ba1 into master 6 years ago
mergify mergify deleted the lint_mathlib branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum