mathlib3
[Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex`
#19236

Closed

[Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex` #19236

eric-wieser wants to merge 4 commits into master from eric-wieser/orientation-reindex

feat(linear_algebra/orientation): add `orientation.reindex`

e1d51f9a

eric-wieser added awaiting-CI

eric-wieser added t-algebra

github-actions added modifies-synchronized-file

orientation_reindex

2eaf3ac1

eric-wieser added awaiting-review

oops

eebeb3a0

github-actions removed awaiting-CI

kim-em added not-too-late

eric-wieser commented on 2023-07-26

Apply suggestions from code review

b5899258

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~feat(linear_algebra/orientation): add `orientation.reindex`~~ [Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex` 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/orientation-reindex branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge t-algebra modifies-synchronized-file not-too-late

Milestone

No milestone

mathlib3 [Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex` #19236 Closed

[Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex` #19236

mathlib3
[Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex`
#19236

Closed