Mathlib v3 is deprecated. Go to Mathlib v4

Theorem projectivization.subspace.mem_span

Modification history

2022-08-16 16:11

src/linear_algebra/projective_space/subspace.lean

feat(linear_algebra/projective_space/subspace): adds lemmas about the span operation and supremums of collections of subspaces (#15596) …

Added projectivization.subspace.mem_span View on Github →