From e88badbfc172c98a0c1a16bb4696b6a77eb2b5c2 Mon Sep 17 00:00:00 2001 From: Daniel Packer <62404584+Daniel-Packer@users.noreply.github.com> Date: Sat, 19 Feb 2022 18:23:35 +0000 Subject: [PATCH] feat(analysis/inner_product_space/pi_L2): Orthonormal basis (#12060) Added the structure orthonormal_basis and basic associated API Renamed the previous definition orthonormal_basis in analysis/inner_product_space/projection to std_orthonormal_basis Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> --- .../inner_product_space/orientation.lean | 4 +- src/analysis/inner_product_space/pi_L2.lean | 167 +++++++++++++++--- .../inner_product_space/projection.lean | 39 ++-- .../inner_product_space/spectrum.lean | 2 +- src/linear_algebra/basis.lean | 9 + 5 files changed, 176 insertions(+), 45 deletions(-) diff --git a/src/analysis/inner_product_space/orientation.lean b/src/analysis/inner_product_space/orientation.lean index 1ef0aad32c72a..a9c97374111ff 100644 --- a/src/analysis/inner_product_space/orientation.lean +++ b/src/analysis/inner_product_space/orientation.lean @@ -37,7 +37,7 @@ protected def orientation.fin_orthonormal_basis {n : ℕ} (hn : 0 < n) (h : finr begin haveI := fin.pos_iff_nonempty.1 hn, haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E), - exact (fin_orthonormal_basis h).adjust_to_orientation x + exact (fin_std_orthonormal_basis h).adjust_to_orientation x end /-- `orientation.fin_orthonormal_basis` is orthonormal. -/ @@ -47,7 +47,7 @@ protected lemma orientation.fin_orthonormal_basis_orthonormal {n : ℕ} (hn : 0 begin haveI := fin.pos_iff_nonempty.1 hn, haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E), - exact (fin_orthonormal_basis_orthonormal h).orthonormal_adjust_to_orientation _ + exact (fin_std_orthonormal_basis_orthonormal h).orthonormal_adjust_to_orientation _ end /-- `orientation.fin_orthonormal_basis` gives a basis with the required orientation. -/ diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean index 08e29e7d3c50c..5417d8481877e 100644 --- a/src/analysis/inner_product_space/pi_L2.lean +++ b/src/analysis/inner_product_space/pi_L2.lean @@ -21,8 +21,11 @@ This is recorded in this file as an inner product space instance on `pi_Lp 2`. from functions to `n` to `𝕜` with the `L²` norm. We register several instances on it (notably that it is a finite-dimensional inner product space). -- `basis.isometry_euclidean_of_orthonormal`: provides the isometry to Euclidean space - from a given finite-dimensional inner product space, induced by a basis of the space. +- `orthonormal_basis 𝕜 ι`: defined to be an isometry to Euclidean space from a given + finite-dimensional innner product space, `E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι`. + +- `basis.to_orthonormal_basis`: constructs an `orthonormal_basis` for a finite-dimensional + Euclidean space from a `basis` which is `orthonormal`. - `linear_isometry_equiv.of_inner_product_space`: provides an arbitrary isometry to Euclidean space from a given finite-dimensional inner product space, induced by choosing an arbitrary basis. @@ -92,7 +95,6 @@ lemma pi_Lp.norm_eq_of_L2 {ι : Type*} [fintype ι] {f : ι → Type*} ∥x∥ = sqrt (∑ (i : ι), ∥x i∥ ^ 2) := by { rw [pi_Lp.norm_eq_of_nat 2]; simp [sqrt_eq_rpow] } - /-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `euclidean_space 𝕜 (fin n)`. -/ @[reducible, nolint unused_arguments] @@ -103,11 +105,11 @@ lemma euclidean_space.norm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [finty (x : euclidean_space 𝕜 n) : ∥x∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) := pi_Lp.norm_eq_of_L2 x +variables [fintype ι] + section local attribute [reducible] pi_Lp -variables [fintype ι] - instance : finite_dimensional 𝕜 (euclidean_space 𝕜 ι) := by apply_instance instance : inner_product_space 𝕜 (euclidean_space 𝕜 ι) := by apply_instance @@ -152,12 +154,111 @@ begin simp [e₂, direct_sum.submodule_coe, direct_sum.to_module, dfinsupp.sum_add_hom_apply] end -/-- An orthonormal basis on a fintype `ι` for an inner product space induces an isometry with +end + +/-- The vector given in euclidean space by being `1 : 𝕜` at coordinate `i : ι` and `0 : 𝕜` at +all other coordinates. -/ +def euclidean_space.single [decidable_eq ι] (i : ι) (a : 𝕜) : + euclidean_space 𝕜 ι := +pi.single i a + +@[simp] theorem euclidean_space.single_apply [decidable_eq ι] (i : ι) (a : 𝕜) (j : ι) : + (euclidean_space.single i a) j = ite (j = i) a 0 := +by { rw [euclidean_space.single, ← pi.single_apply i a j] } + +lemma euclidean_space.inner_single_left [decidable_eq ι] (i : ι) (a : 𝕜) (v : euclidean_space 𝕜 ι) : + ⟪euclidean_space.single i (a : 𝕜), v⟫ = conj a * (v i) := +by simp [apply_ite conj] + +lemma euclidean_space.inner_single_right [decidable_eq ι] (i : ι) (a : 𝕜) + (v : euclidean_space 𝕜 ι) : + ⟪v, euclidean_space.single i (a : 𝕜)⟫ = a * conj (v i) := +by simp [apply_ite conj, mul_comm] + +variables (ι 𝕜 E) + +/-- An orthonormal basis on E is an identification of `E` with its dimensional-matching `euclidean_space 𝕜 ι`. -/ -def basis.isometry_euclidean_of_orthonormal - (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : - E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι := -v.equiv_fun.isometry_of_inner +structure orthonormal_basis := of_repr :: (repr : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι) + +variables {ι 𝕜 E} + +namespace orthonormal_basis + +instance : inhabited (orthonormal_basis ι 𝕜 (euclidean_space 𝕜 ι)) := +⟨of_repr (linear_isometry_equiv.refl 𝕜 (euclidean_space 𝕜 ι))⟩ + +/-- `b i` is the `i`th basis vector. -/ +instance : has_coe_to_fun (orthonormal_basis ι 𝕜 E) (λ _, ι → E) := +{ coe := λ b i, by classical; exact b.repr.symm (euclidean_space.single i (1 : 𝕜)) } + +@[simp] protected lemma repr_symm_single [decidable_eq ι] (b : orthonormal_basis ι 𝕜 E) (i : ι) : + b.repr.symm (euclidean_space.single i (1:𝕜)) = b i := +by { classical, congr, simp, } + +@[simp] protected lemma repr_self [decidable_eq ι] (b : orthonormal_basis ι 𝕜 E) (i : ι) : + b.repr (b i) = euclidean_space.single i (1:𝕜) := +begin + classical, + rw [← b.repr_symm_single i, linear_isometry_equiv.apply_symm_apply], + congr, + simp, +end + +protected lemma repr_apply_apply (b : orthonormal_basis ι 𝕜 E) (v : E) (i : ι) : + b.repr v i = ⟪b i, v⟫ := +begin + classical, + rw [← b.repr.inner_map_map (b i) v, b.repr_self i, euclidean_space.inner_single_left], + simp only [one_mul, eq_self_iff_true, map_one], +end + +@[simp] +protected lemma orthonormal (b : orthonormal_basis ι 𝕜 E) : orthonormal 𝕜 b := +begin + classical, + rw orthonormal_iff_ite, + intros i j, + rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j], + rw euclidean_space.inner_single_left, + rw euclidean_space.single_apply, + simp only [mul_boole, map_one], +end + +/-- The `basis ι 𝕜 E` underlying the `orthonormal_basis` --/ +protected def to_basis (b : orthonormal_basis ι 𝕜 E) : basis ι 𝕜 E := +basis.of_equiv_fun b.repr.to_linear_equiv + +@[simp] protected lemma coe_to_basis (b : orthonormal_basis ι 𝕜 E) : + (⇑b.to_basis : ι → E) = ⇑b := +begin + change ⇑(basis.of_equiv_fun b.repr.to_linear_equiv) = b, + ext j, + rw basis.coe_of_equiv_fun, + simp only [orthonormal_basis.repr_symm_single], + congr, +end + +@[simp] protected lemma coe_to_basis_repr (b : orthonormal_basis ι 𝕜 E) : + b.to_basis.equiv_fun = b.repr.to_linear_equiv := +begin + change (basis.of_equiv_fun b.repr.to_linear_equiv).equiv_fun = b.repr.to_linear_equiv, + ext x j, + simp only [basis.of_equiv_fun_repr_apply, eq_self_iff_true, + linear_isometry_equiv.coe_to_linear_equiv, basis.equiv_fun_apply], +end + +protected lemma sum_repr_symm (b : orthonormal_basis ι 𝕜 E) (v : euclidean_space 𝕜 ι) : + ∑ i , v i • b i = (b.repr.symm v) := +by { classical, simpa using (b.to_basis.equiv_fun_symm_apply v).symm } + +variable {v : ι → E} + +/-- A basis that is orthonormal is an orthonormal basis. -/ +def _root_.basis.to_orthonormal_basis (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : + orthonormal_basis ι 𝕜 E := +orthonormal_basis.of_repr $ +linear_equiv.isometry_of_inner v.equiv_fun begin intros x y, let p : euclidean_space 𝕜 ι := v.equiv_fun x, @@ -169,37 +270,56 @@ begin { rw [← v.equiv_fun.symm_apply_apply y, v.equiv_fun_symm_apply] } end -@[simp] lemma basis.coe_isometry_euclidean_of_orthonormal - (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : - (v.isometry_euclidean_of_orthonormal hv : E → euclidean_space 𝕜 ι) = v.equiv_fun := +@[simp] lemma _root_.basis.coe_to_orthonormal_basis_repr (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : + ((v.to_orthonormal_basis hv).repr : E → euclidean_space 𝕜 ι) = v.equiv_fun := rfl -@[simp] lemma basis.coe_isometry_euclidean_of_orthonormal_symm +@[simp] lemma _root_.basis.coe_to_orthonormal_basis_repr_symm (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : - ((v.isometry_euclidean_of_orthonormal hv).symm : euclidean_space 𝕜 ι → E) = v.equiv_fun.symm := + ((v.to_orthonormal_basis hv).repr.symm : euclidean_space 𝕜 ι → E) = v.equiv_fun.symm := rfl +@[simp] lemma _root_.basis.to_basis_to_orthonormal_basis (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : + (v.to_orthonormal_basis hv).to_basis = v := +by simp [basis.to_orthonormal_basis, orthonormal_basis.to_basis] + +@[simp] lemma _root_.basis.coe_to_orthonormal_basis (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) : + (v.to_orthonormal_basis hv : ι → E) = (v : ι → E) := +calc (v.to_orthonormal_basis hv : ι → E) = ((v.to_orthonormal_basis hv).to_basis : ι → E) : + by { classical, rw orthonormal_basis.coe_to_basis } +... = (v : ι → E) : by simp + +/-- An orthonormal set that spans is an orthonormal basis -/ +protected def mk (hon : orthonormal 𝕜 v) (hsp: submodule.span 𝕜 (set.range v) = ⊤): + orthonormal_basis ι 𝕜 E := +(basis.mk (orthonormal.linear_independent hon) hsp).to_orthonormal_basis (by rwa basis.coe_mk) + +@[simp] +protected lemma coe_mk (hon : orthonormal 𝕜 v) (hsp: submodule.span 𝕜 (set.range v) = ⊤) : + ⇑(orthonormal_basis.mk hon hsp) = v := +by classical; rw [orthonormal_basis.mk, _root_.basis.coe_to_orthonormal_basis, basis.coe_mk] + +end orthonormal_basis + /-- If `f : E ≃ₗᵢ[𝕜] E'` is a linear isometry of inner product spaces then an orthonormal basis `v` of `E` determines a linear isometry `e : E' ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι`. This result states that `e` may be obtained either by transporting `v` to `E'` or by composing with the linear isometry `E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι` provided by `v`. -/ @[simp] lemma basis.map_isometry_euclidean_of_orthonormal (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) (f : E ≃ₗᵢ[𝕜] E') : - (v.map f.to_linear_equiv).isometry_euclidean_of_orthonormal (hv.map_linear_isometry_equiv f) = - f.symm.trans (v.isometry_euclidean_of_orthonormal hv) := + ((v.map f.to_linear_equiv).to_orthonormal_basis (hv.map_linear_isometry_equiv f)).repr = + f.symm.trans (v.to_orthonormal_basis hv).repr := linear_isometry_equiv.to_linear_equiv_injective $ v.map_equiv_fun _ -end - /-- `ℂ` is isometric to `ℝ²` with the Euclidean inner product. -/ def complex.isometry_euclidean : ℂ ≃ₗᵢ[ℝ] (euclidean_space ℝ (fin 2)) := -complex.basis_one_I.isometry_euclidean_of_orthonormal +(complex.basis_one_I.to_orthonormal_basis begin rw orthonormal_iff_ite, intros i, fin_cases i; intros j; fin_cases j; simp [real_inner_eq_re_inner] -end +end).repr @[simp] lemma complex.isometry_euclidean_symm_apply (x : euclidean_space ℝ (fin 2)) : complex.isometry_euclidean.symm x = (x 0) + (x 1) * I := @@ -224,7 +344,7 @@ by { conv_rhs { rw ← complex.isometry_euclidean_proj_eq_self z }, simp } /-- The isometry between `ℂ` and a two-dimensional real inner product space given by a basis. -/ def complex.isometry_of_orthonormal {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ v) : ℂ ≃ₗᵢ[ℝ] F := -complex.isometry_euclidean.trans (v.isometry_euclidean_of_orthonormal hv).symm +complex.isometry_euclidean.trans (v.to_orthonormal_basis hv).repr.symm @[simp] lemma complex.map_isometry_of_orthonormal {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ v) (f : F ≃ₗᵢ[ℝ] F') : @@ -249,7 +369,8 @@ there exists an isometry from the space to `euclidean_space 𝕜 (fin n)`. -/ def linear_isometry_equiv.of_inner_product_space [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) : E ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) := -(fin_orthonormal_basis hn).isometry_euclidean_of_orthonormal (fin_orthonormal_basis_orthonormal hn) +((fin_std_orthonormal_basis hn).to_orthonormal_basis + (fin_std_orthonormal_basis_orthonormal hn)).repr local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ diff --git a/src/analysis/inner_product_space/projection.lean b/src/analysis/inner_product_space/projection.lean index 05e35cf8be67e..d539654b71130 100644 --- a/src/analysis/inner_product_space/projection.lean +++ b/src/analysis/inner_product_space/projection.lean @@ -1143,37 +1143,38 @@ variables (𝕜 E) def orthonormal_basis_index : set E := classical.some (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)) + /-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/ -def orthonormal_basis : +def std_orthonormal_basis : basis (orthonormal_basis_index 𝕜 E) 𝕜 E := (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some -lemma orthonormal_basis_orthonormal : - orthonormal 𝕜 (orthonormal_basis 𝕜 E) := +lemma std_orthonormal_basis_orthonormal : + orthonormal 𝕜 (std_orthonormal_basis 𝕜 E) := (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.1 -@[simp] lemma coe_orthonormal_basis : - ⇑(orthonormal_basis 𝕜 E) = coe := +@[simp] lemma coe_std_orthonormal_basis : + ⇑(std_orthonormal_basis 𝕜 E) = coe := (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2 instance : fintype (orthonormal_basis_index 𝕜 E) := @is_noetherian.fintype_basis_index _ _ _ _ _ _ _ - (is_noetherian.iff_fg.2 infer_instance) (orthonormal_basis 𝕜 E) + (is_noetherian.iff_fg.2 infer_instance) (std_orthonormal_basis 𝕜 E) variables {𝕜 E} /-- An `n`-dimensional `inner_product_space` has an orthonormal basis indexed by `fin n`. -/ -def fin_orthonormal_basis {n : ℕ} (hn : finrank 𝕜 E = n) : +def fin_std_orthonormal_basis {n : ℕ} (hn : finrank 𝕜 E = n) : basis (fin n) 𝕜 E := have h : fintype.card (orthonormal_basis_index 𝕜 E) = n, -by rw [← finrank_eq_card_basis (orthonormal_basis 𝕜 E), hn], -(orthonormal_basis 𝕜 E).reindex (fintype.equiv_fin_of_card_eq h) +by rw [← finrank_eq_card_basis (std_orthonormal_basis 𝕜 E), hn], +(std_orthonormal_basis 𝕜 E).reindex (fintype.equiv_fin_of_card_eq h) -lemma fin_orthonormal_basis_orthonormal {n : ℕ} (hn : finrank 𝕜 E = n) : - orthonormal 𝕜 (fin_orthonormal_basis hn) := -suffices orthonormal 𝕜 (orthonormal_basis _ _ ∘ equiv.symm _), -by { simp only [fin_orthonormal_basis, basis.coe_reindex], assumption }, -- why doesn't simpa work? -(orthonormal_basis_orthonormal 𝕜 E).comp _ (equiv.injective _) +lemma fin_std_orthonormal_basis_orthonormal {n : ℕ} (hn : finrank 𝕜 E = n) : + orthonormal 𝕜 (fin_std_orthonormal_basis hn) := +suffices orthonormal 𝕜 (std_orthonormal_basis _ _ ∘ equiv.symm _), +by { simp only [fin_std_orthonormal_basis, basis.coe_reindex], assumption }, -- simpa doesn't work? +(std_orthonormal_basis_orthonormal 𝕜 E).comp _ (equiv.injective _) section subordinate_orthonormal_basis open direct_sum @@ -1184,14 +1185,14 @@ variables {n : ℕ} (hn : finrank 𝕜 E = n) {ι : Type*} [fintype ι] [decidab inner product space `E`. This should not be accessed directly, but only via the subsequent API. -/ @[irreducible] def direct_sum.submodule_is_internal.sigma_orthonormal_basis_index_equiv : (Σ i, orthonormal_basis_index 𝕜 (V i)) ≃ fin n := -let b := hV.collected_basis (λ i, orthonormal_basis 𝕜 (V i)) in +let b := hV.collected_basis (λ i, std_orthonormal_basis 𝕜 (V i)) in fintype.equiv_fin_of_card_eq $ (finite_dimensional.finrank_eq_card_basis b).symm.trans hn /-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. -/ @[irreducible] def direct_sum.submodule_is_internal.subordinate_orthonormal_basis : basis (fin n) 𝕜 E := -(hV.collected_basis (λ i, orthonormal_basis 𝕜 (V i))).reindex +(hV.collected_basis (λ i, std_orthonormal_basis 𝕜 (V i))).reindex (hV.sigma_orthonormal_basis_index_equiv hn) /-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct @@ -1206,8 +1207,8 @@ lemma direct_sum.submodule_is_internal.subordinate_orthonormal_basis_orthonormal orthonormal 𝕜 (hV.subordinate_orthonormal_basis hn) := begin simp only [direct_sum.submodule_is_internal.subordinate_orthonormal_basis, basis.coe_reindex], - have : orthonormal 𝕜 (hV.collected_basis (λ i, orthonormal_basis 𝕜 (V i))) := - hV.collected_basis_orthonormal hV' (λ i, orthonormal_basis_orthonormal 𝕜 (V i)), + have : orthonormal 𝕜 (hV.collected_basis (λ i, std_orthonormal_basis 𝕜 (V i))) := + hV.collected_basis_orthonormal hV' (λ i, std_orthonormal_basis_orthonormal 𝕜 (V i)), exact this.comp _ (equiv.injective _), end @@ -1216,7 +1217,7 @@ the `orthogonal_family` in question. -/ lemma direct_sum.submodule_is_internal.subordinate_orthonormal_basis_subordinate (a : fin n) : hV.subordinate_orthonormal_basis hn a ∈ V (hV.subordinate_orthonormal_basis_index hn a) := by simpa only [direct_sum.submodule_is_internal.subordinate_orthonormal_basis, basis.coe_reindex] - using hV.collected_basis_mem (λ i, orthonormal_basis 𝕜 (V i)) + using hV.collected_basis_mem (λ i, std_orthonormal_basis 𝕜 (V i)) ((hV.sigma_orthonormal_basis_index_equiv hn).symm a) attribute [irreducible] direct_sum.submodule_is_internal.subordinate_orthonormal_basis_index diff --git a/src/analysis/inner_product_space/spectrum.lean b/src/analysis/inner_product_space/spectrum.lean index ad3cca6d234c9..3586b731d0dd4 100644 --- a/src/analysis/inner_product_space/spectrum.lean +++ b/src/analysis/inner_product_space/spectrum.lean @@ -219,7 +219,7 @@ mem_eigenspace_iff.mp (hT.has_eigenvector_eigenvector_basis hn i).1 /-- An isometry from an inner product space `E` to Euclidean space, induced by a choice of orthonormal basis of eigenvectors for a self-adjoint operator `T` on `E`. -/ noncomputable def diagonalization_basis : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 (fin n) := -(hT.eigenvector_basis hn).isometry_euclidean_of_orthonormal (hT.eigenvector_basis_orthonormal hn) +((hT.eigenvector_basis hn).to_orthonormal_basis (hT.eigenvector_basis_orthonormal hn)).repr @[simp] lemma diagonalization_basis_symm_apply (w : euclidean_space 𝕜 (fin n)) : (hT.diagonalization_basis hn).symm w = ∑ i, w i • hT.eigenvector_basis hn i := diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean index df4954c8c8fe2..b0564cf382f04 100644 --- a/src/linear_algebra/basis.lean +++ b/src/linear_algebra/basis.lean @@ -774,6 +774,15 @@ basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_fintyp funext $ λ i, e.injective $ funext $ λ j, by simp [basis.of_equiv_fun, ←finsupp.single_eq_pi_single, finsupp.single_eq_update] +@[simp] lemma basis.of_equiv_fun_equiv_fun + (v : basis ι R M) : basis.of_equiv_fun v.equiv_fun = v := +begin + ext j, + simp only [basis.equiv_fun_symm_apply, basis.coe_of_equiv_fun], + simp_rw [function.update_apply, ite_smul], + simp only [finset.mem_univ, if_true, pi.zero_apply, one_smul, finset.sum_ite_eq', zero_smul], +end + variables (S : Type*) [semiring S] [module S M'] variables [smul_comm_class R S M']