minpoly): remove a silly use of `tauto`
#19183

Closed

[Merged by Bors] - chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto` #19183

eric-wieser wants to merge 3 commits into master from eric-wieser/tiny-golf

chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto`

c7a90a9d

eric-wieser added easy

eric-wieser added awaiting-review

eric-wieser added awaiting-CI

github-actions added modifies-synchronized-file

github-actions removed awaiting-CI

Merge branch 'master' into eric-wieser/tiny-golf

f4ef26f4

eric-wieser commented on 2023-06-13

Update src/linear_algebra/eigenspace/minpoly.lean

74780658

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto`~~ [Merged by Bors] - chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto` 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/tiny-golf branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge easy modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto` #19183 Closed

[Merged by Bors] - chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto` #19183

mathlib3
[Merged by Bors] - chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto`
#19183

Closed