Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-05-25 02:59
10878f6b
View on Github →
feat(linear_algebra/span): generalise to_span_nonzero_singleton (
#19082
)
Estimated changes
Modified
src/linear_algebra/span.lean
modified
def
linear_equiv.coord
added
theorem
linear_equiv.coord_apply_smul
modified
theorem
linear_equiv.coord_self
modified
def
linear_equiv.to_span_nonzero_singleton
modified
theorem
linear_equiv.to_span_nonzero_singleton_one
modified
theorem
linear_map.ker_to_span_singleton