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>

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. -/

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
 

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

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 :=

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']