chore: forward-port leanprover-community/mathlib3#19021 (leanprover-c…

…ommunity#4257)
qawbecrdtey · Jun 12, 2023 · a7a6bb9 · a7a6bb9
1 parent c422cf4
commit a7a6bb9
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 2 deletions.
diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 
 ! This file was ported from Lean 3 source module linear_algebra.basis
-! leanprover-community/mathlib commit 04cdee31e196e30f507e8e9eb2d06e02c9ff6310
+! leanprover-community/mathlib commit 13bce9a6b6c44f6b4c91ac1c1d2a816e2533d395
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -980,6 +980,12 @@ theorem Basis.ofEquivFun_equivFun (v : Basis ι R M) : Basis.ofEquivFun v.equivF
     simp only [Finset.mem_univ, if_true, Pi.zero_apply, one_smul, Finset.sum_ite_eq', zero_smul]
 #align basis.of_equiv_fun_equiv_fun Basis.ofEquivFun_equivFun
 
+@[simp]
+theorem Basis.equivFun_ofEquivFun (e : M ≃ₗ[R] ι → R) : (Basis.ofEquivFun e).equivFun = e := by
+  ext j
+  simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]
+#align basis.equiv_fun_of_equiv_fun Basis.equivFun_ofEquivFun
+
 variable (S : Type _) [Semiring S] [Module S M']
 
 variable [SMulCommClass R S M']

diff --git a/Mathlib/LinearAlgebra/StdBasis.lean b/Mathlib/LinearAlgebra/StdBasis.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module linear_algebra.std_basis
-! leanprover-community/mathlib commit f8c79b0a623404854a2902b836eac32156fd7712
+! leanprover-community/mathlib commit 13bce9a6b6c44f6b4c91ac1c1d2a816e2533d395
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -289,6 +289,11 @@ theorem basisFun_apply [DecidableEq η] (i) : basisFun R η i = stdBasis R (fun
 theorem basisFun_repr (x : η → R) (i : η) : (Pi.basisFun R η).repr x i = x i := by simp [basisFun]
 #align pi.basis_fun_repr Pi.basisFun_repr
 
+@[simp]
+theorem basisFun_equivFun : (Pi.basisFun R η).equivFun = LinearEquiv.refl _ _ :=
+  Basis.equivFun_ofEquivFun _
+#align pi.basis_fun_equiv_fun Pi.basisFun_equivFun
+
 end
 
 end Module