feat(linear_algebra/basis) remove several [nontrivial R] (#7642)

We remove some unnecessary `nontrivial R`.

Author: riccardobrasca

src/linear_algebra/basis.lean

@@ -230,6 +230,18 @@ repr_eq_iff'.mpr (λ i, by rw [h, b₂.repr_self])
 
 end ext
 
+section map
+
+variables (f : M ≃ₗ[R] M')
+
+/-- Apply the linear equivalence `f` to the basis vectors. -/
+protected def map : basis ι R M' :=
+of_repr (f.symm.trans b.repr)
+
+@[simp] lemma map_apply (i) : b.map f i = f (b i) := rfl
+
+end map
+
 section reindex
 
 variables (b' : basis ι' R M')
@@ -263,31 +275,44 @@ lemma range_reindex : set.range (b.reindex e) = set.range b :=
 by rw [coe_reindex, range_reindex']
 
 /-- `b.reindex_range` is a basis indexed by `range b`, the basis vectors themselves. -/
-def reindex_range [nontrivial R] : basis (range b) R M :=
-b.reindex (equiv.of_injective b b.injective)
+def reindex_range : basis (range b) R M :=
+if h : nontrivial R then
+  by letI := h; exact b.reindex (equiv.of_injective b (basis.injective b))
+else
+  by letI : subsingleton R := not_nontrivial_iff_subsingleton.mp h; exact
+    basis.of_repr (module.subsingleton_equiv R M (range b))
 
 lemma finsupp.single_apply_left {α β γ : Type*} [has_zero γ]
   {f : α → β} (hf : function.injective f)
   (x z : α) (y : γ) :
   finsupp.single (f x) y (f z) = finsupp.single x y z :=
 by simp [finsupp.single_apply, hf.eq_iff]
 
-lemma reindex_range_self [nontrivial R] (i : ι) (h := set.mem_range_self i) :
+lemma reindex_range_self (i : ι) (h := set.mem_range_self i) :
   b.reindex_range ⟨b i, h⟩ = b i :=
-by rw [reindex_range, reindex_apply, equiv.apply_of_injective_symm b b.injective, subtype.coe_mk]
+begin
+  by_cases htr : nontrivial R,
+  { letI := htr,
+    simp [htr, reindex_range, reindex_apply, equiv.apply_of_injective_symm b b.injective,
+      subtype.coe_mk] },
+  { letI : subsingleton R := not_nontrivial_iff_subsingleton.mp htr,
+    letI := module.subsingleton R M,
+    simp [reindex_range] }
+end
 
-lemma reindex_range_repr_self [nontrivial R] (i : ι) :
+lemma reindex_range_repr_self (i : ι) :
   b.reindex_range.repr (b i) = finsupp.single ⟨b i, mem_range_self i⟩ 1 :=
 calc b.reindex_range.repr (b i) = b.reindex_range.repr (b.reindex_range ⟨b i, mem_range_self i⟩) :
   congr_arg _ (b.reindex_range_self _ _).symm
 ... = finsupp.single ⟨b i, mem_range_self i⟩ 1 : b.reindex_range.repr_self _
 
-@[simp] lemma reindex_range_apply [nontrivial R] (x : range b) : b.reindex_range x = x :=
+@[simp] lemma reindex_range_apply (x : range b) : b.reindex_range x = x :=
 by { rcases x with ⟨bi, ⟨i, rfl⟩⟩, exact b.reindex_range_self i, }
 
-lemma reindex_range_repr' [nontrivial R] (x : M) {bi : M} {i : ι} (h : b i = bi) :
+lemma reindex_range_repr' (x : M) {bi : M} {i : ι} (h : b i = bi) :
   b.reindex_range.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i :=
 begin
+  nontriviality,
   subst h,
   refine (b.repr_apply_eq (λ x i, b.reindex_range.repr x ⟨b i, _⟩) _ _ _ x i).symm,
   { intros x y,
@@ -303,7 +328,7 @@ begin
     exact λ i j h, b.injective (subtype.mk.inj h) }
 end
 
-@[simp] lemma reindex_range_repr [nontrivial R] (x : M) (i : ι) (h := set.mem_range_self i) :
+@[simp] lemma reindex_range_repr (x : M) (i : ι) (h := set.mem_range_self i) :
   b.reindex_range.repr x ⟨b i, h⟩ = b.repr x i :=
 b.reindex_range_repr' _ rfl
 
@@ -400,18 +425,6 @@ b.ext' (λ i, by simp)
 
 end equiv
 
-section map
-
-variables (f : M ≃ₗ[R] M')
-
-/-- Apply the linear equivalence `f` to the basis vectors. -/
-protected def map : basis ι R M' :=
-of_repr (f.symm.trans b.repr)
-
-@[simp] lemma map_apply (i) : b.map f i = f (b i) := rfl
-
-end map
-
 section prod
 
 variables (b' : basis ι' R M')

src/linear_algebra/finsupp.lean

@@ -809,3 +809,14 @@ begin
   simp_rw ←exists_prop,
   exact finsupp.mem_span_iff_total R,
 end
+
+/-- If `subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/
+@[simps]
+def module.subsingleton_equiv (R M ι: Type*) [semiring R] [subsingleton R] [add_comm_monoid M]
+  [module R M] : M ≃ₗ[R] ι →₀ R :=
+{ to_fun := λ m, 0,
+  inv_fun := λ f, 0,
+  left_inv := λ m, by { letI := module.subsingleton R M, simp only [eq_iff_true_of_subsingleton] },
+  right_inv := λ f, by simp only [eq_iff_true_of_subsingleton],
+  map_add' := λ m n, (add_zero 0).symm,
+  map_smul' := λ r m, (smul_zero r).symm }

src/linear_algebra/matrix/to_lin.lean

@@ -307,7 +307,7 @@ linear_map.to_matrix_id v₁
 lemma matrix.to_lin_one : matrix.to_lin v₁ v₁ 1 = id :=
 by rw [← linear_map.to_matrix_id v₁, matrix.to_lin_to_matrix]
 
-theorem linear_map.to_matrix_reindex_range [nontrivial R] [decidable_eq M₁] [decidable_eq M₂]
+theorem linear_map.to_matrix_reindex_range [decidable_eq M₁] [decidable_eq M₂]
   (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
   linear_map.to_matrix v₁.reindex_range v₂.reindex_range f
       ⟨v₂ k, mem_range_self k⟩ ⟨v₁ i, mem_range_self i⟩ =
@@ -407,7 +407,7 @@ by simp_rw [linear_map.to_matrix_alg_equiv, alg_equiv.of_linear_equiv_apply,
 lemma matrix.to_lin_alg_equiv_one : matrix.to_lin_alg_equiv v₁ 1 = id :=
 by rw [← linear_map.to_matrix_alg_equiv_id v₁, matrix.to_lin_alg_equiv_to_matrix_alg_equiv]
 
-theorem linear_map.to_matrix_alg_equiv_reindex_range [nontrivial R] [decidable_eq M₁]
+theorem linear_map.to_matrix_alg_equiv_reindex_range [decidable_eq M₁]
   (f : M₁ →ₗ[R] M₁) (k i : n) :
   linear_map.to_matrix_alg_equiv v₁.reindex_range f
       ⟨v₁ k, mem_range_self k⟩ ⟨v₁ i, mem_range_self i⟩ =