mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open vbeffara opened this issue 3 years ago • 0 comments

A few basic lemmas and definitions, with a few special cases for the projective line (as P K (K \times K).

Open in Gitpod

vbeffara avatar May 10 '22 08:05 vbeffara