Commit 2023-06-08 12:59 e06ec219

View on Github →

chore: forward-port leanprover-community/mathlib#19082 (#4816)

Estimated changes

Modified Mathlib/LinearAlgebra/Span.lean

added theorem LinearEquiv.coord_apply_smul

modified theorem LinearEquiv.coord_self

modified def LinearEquiv.toSpanNonzeroSingleton

modified theorem LinearEquiv.toSpanNonzeroSingleton_one

modified theorem LinearMap.ker_toSpanSingleton