mathlib3
feat(linear_algebra/projective_space): add some basic API and instances
#14059

Open

feat(linear_algebra/projective_space): add some basic API and instances #14059

vbeffara wants to merge 5 commits into master from VB_proj

feat(linear_algebra/projective_space): add some basic API and instance

c4afaddc

vbeffara requested a review from

adamtopaz 3 years ago

vbeffara added awaiting-review

eric-wieser commented on 2022-05-10

Refactor map_injective

bed4b55b

riccardobrasca commented on 2022-05-12

Update src/linear_algebra/projective_space/basic.lean

7d20820a

Update src/linear_algebra/projective_space/basic.lean

ff19d9de

ocfnash commented on 2022-05-24

ocfnash removed awaiting-review

ocfnash added awaiting-author

Update src/linear_algebra/projective_space/basic.lean

6cfb65ff

kim-em added too-late

Reviewers

ocfnash

riccardobrasca

eric-wieser

adamtopaz

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone