[Merged by Bors] - feat(linear_algebra): elements of a dim zero space #3054
Conversation
robertylewis
added
the
awaiting-review
src/linear_algebra/dimension.lean
Outdated
| @@ -412,6 +412,14 @@ by rw [rank, rank, linear_map.range_comp]; exact dim_map_le _ _ | |||
|
|
|||
| end rank | |||
|
|
|||
| lemma eq_zero_of_dim_zero (h : vector_space.dim K V = 0) (x : V) : x = 0 := | |||
There was a problem hiding this comment.
We could also have the iff variation: dimension is zero iff every vector is zero. Otherwise this looks good to me (and not having these lemmas when you need them is certainly annoying).
There was a problem hiding this comment.
@hrmacbeth has (the contrapositive of) that in #3021. To be honest I'm not really sure which statement would be the most useful.
There was a problem hiding this comment.
The iff version is nice and clean; why don't you do that, and I'll adjust my PR accordingly?
There was a problem hiding this comment.
And one other variant: the contrapositive of your current statement is (∃ b : V, b ≠ 0) → (vector_space.dim K V ≠ 0), but for convenience maybe it would be nice to have a version with the conclusion vector_space.dim K V > 0.
There was a problem hiding this comment.
Okay, I've made it into an iff. And with a little update to push_neg (cc @PatrickMassot), I have the useful contrapositive version as well, subsuming the version in #3021.
There was a problem hiding this comment.
Never mind, the push_neg change wasn't actually needed.
|
bors merge |
github-actions
bot
added
ready-to-merge
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…ity#3054) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
I haven't touched linear algebra in a while; this came up in #3021 so I gave it a shot. A few related but unused lemmas also.