PR #2287 doc(algebra/group/type_tags): add docs

doc(algebra/group/type_tags): add docs #2287

mergify merged 3 commits into master from mult-add-docs

doc(algebra/group/type_tags): add docs

b15aa8e9

bryangingechen approved these changes on 2020-03-30

bryangingechen added ready-to-merge

Merge branch 'master' into mult-add-docs

5efa39f8

sgouezel commented on 2020-03-30

Update src/algebra/group/type_tags.lean

ef6d7724

mergify merged 3f0e700c into master 6 years ago

urkud deleted the mult-add-docs branch 6 years ago

Reviewers

bryangingechen

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone