mathlib3
feat(data/matrix/companion): Companion matrix
#15047
Open
Overview
Commits
5
Changes
View On GitHub

feat(data/matrix/companion): Companion matrix #15047

pbazin wants to merge 5 commits into master from companion_matrix'
pbazin
pbazin companion matrix
e229016a
pbazin fin.last'
32ffa13c
eric-wieser
eric-wieser commented on 2022-06-29
pbazin minpoly
ba2ccf27
pbazin doc
45a00561
vihdzp
vihdzp commented on 2022-06-30
pbazin simp lemmas from companion def
3a57527c
YaelDillies YaelDillies changed the title feat(data/matrix/companion.lean): define companion matrix feat(data/matrix/companion): Companion matrix 3 years ago
kim-em
eric-wieser
eric-wieser commented on 2023-03-30
kim-em kim-em added not-too-late
kim-em kim-em removed not-too-late
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum