Commit 2023-04-28 17:46 16eabc47

View on Github →

feat LinearAlgebra.Basis: add basis.restrictScalars (#3707) Mathlib4 version of https://github.com/leanprover-community/mathlib/pull/18814 linear_algebra.basis@2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e..04cdee31e196e30f507e8e9eb2d06e02c9ff6310)

Estimated changes

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.mem_span_iff_repr_mem

added theorem Basis.restrictScalars_apply

added theorem Basis.restrictScalars_repr_apply