mathlib3
refactor(data/multiset): rename diagonal to antidiagonal
#1236
Merged
Overview
Commits
6
Changes
View On GitHub

refactor(data/multiset): rename diagonal to antidiagonal #1236

mergify merged 6 commits into master from antidiagonal
jcommelin
jcommelin refactor(data/multiset): rename diagonal to antidiagonal
b412fe6d
jcommelin jcommelin requested a review 6 years ago
digama0
digama0 approved these changes on 2019-07-16
ChrisHughes24
jcommelin Add docstrings
d086f464
ChrisHughes24 ChrisHughes24 added ready-to-merge
ChrisHughes24 Merge branch 'master' into antidiagonal
1fa59a1a
ChrisHughes24 fix build
fde22668
jcommelin Fix build
16ce159a
mergify[bot] Merge branch 'master' into antidiagonal
d2c6b292
mergify mergify merged 8785bd0f into master 6 years ago
mergify mergify deleted the antidiagonal 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