chore(linear_algebra/basis): replace explicit arguments for 0 ≠ 1 with nontrivial R (#3678)

Author: TwoFX

archive/sensitivity.lean

@@ -369,7 +369,7 @@ begin
     have hdW := dim_span li,
     rw set.range_restrict at hdW,
     convert hdW,
-    rw [cardinal.mk_image_eq ((dual_pair_e_ε _).is_basis.injective zero_ne_one), cardinal.fintype_card] },
+    rw [cardinal.mk_image_eq (dual_pair_e_ε _).is_basis.injective, cardinal.fintype_card] },
   rw ← findim_eq_dim ℝ at ⊢ dim_le dim_add dimW,
   rw [← findim_eq_dim ℝ, ← findim_eq_dim ℝ] at dim_add,
   norm_cast at ⊢ dim_le dim_add dimW,

src/linear_algebra/basis.lean

@@ -125,9 +125,9 @@ begin
  exact false.elim (not_nonempty_iff_imp_false.1 h i)
 end
 
-lemma linear_independent.ne_zero
-  {i : ι} (ne : 0 ≠ (1:R)) (hv : linear_independent R v) : v i ≠ 0 :=
-λ h, ne $ eq.symm begin
+lemma linear_independent.ne_zero [nontrivial R]
+  {i : ι} (hv : linear_independent R v) : v i ≠ 0 :=
+λ h, @zero_ne_one R _ _ $ eq.symm begin
   suffices : (finsupp.single i 1 : ι →₀ R) i = 0, {simpa},
   rw linear_independent_iff.1 hv (finsupp.single i 1),
   {simp},
@@ -153,7 +153,7 @@ lemma linear_independent.unique (hv : linear_independent R v) {l₁ l₂ : ι 
   finsupp.total ι M R v l₁ = finsupp.total ι M R v l₂ → l₁ = l₂ :=
 by apply linear_map.ker_eq_bot.1 hv
 
-lemma linear_independent.injective (zero_ne_one : (0 : R) ≠ 1) (hv : linear_independent R v) :
+lemma linear_independent.injective [nontrivial R] (hv : linear_independent R v) :
   injective v :=
 begin
   intros i j hij,
@@ -254,12 +254,13 @@ lemma linear_independent.to_subtype_range
 begin
   by_cases zero_eq_one : (0 : R) = 1,
   { apply linear_independent_of_zero_eq_one zero_eq_one },
+  haveI : nontrivial R := ⟨⟨0, 1, zero_eq_one⟩⟩,
   rw linear_independent_subtype,
   intros l hl₁ hl₂,
   have h_bij : bij_on v (v ⁻¹' ↑l.support) ↑l.support,
   { apply bij_on.mk,
     { apply maps_to_preimage },
-    { apply (linear_independent.injective zero_eq_one hv).inj_on },
+    { apply (linear_independent.injective hv).inj_on },
     intros x hx,
     rcases mem_range.1 (((finsupp.mem_supported _ _).1 hl₁ : ↑(l.support) ⊆ range v) hx)
       with ⟨i, hi⟩,
@@ -424,12 +425,13 @@ lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
 begin
   by_cases zero_eq_one : (0 : R) = 1,
   { apply linear_independent_of_zero_eq_one zero_eq_one },
+  haveI : nontrivial R := ⟨⟨0, 1, zero_eq_one⟩⟩,
   apply linear_independent.of_subtype_range,
   { rintros ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy,
     by_cases h_cases : x₁ = y₁,
     subst h_cases,
     { apply sigma.eq,
-      rw linear_independent.injective zero_eq_one (hindep _) hxy,
+      rw linear_independent.injective (hindep _) hxy,
       refl },
     { have h0 : f x₁ x₂ = 0,
       { apply disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁)
@@ -438,7 +440,7 @@ begin
         simp only at hxy,
         rw hxy,
         exact (subset_span (mem_range_self y₂)) },
-      exact false.elim ((hindep x₁).ne_zero zero_eq_one h0) } },
+      exact false.elim ((hindep x₁).ne_zero h0) } },
   rw range_sigma_eq_Union_range,
   apply linear_independent_Union_finite_subtype (λ j, (hindep j).to_subtype_range) hd,
 end
@@ -534,9 +536,9 @@ end⟩
 
 end repr
 
-lemma surjective_of_linear_independent_of_span
+lemma surjective_of_linear_independent_of_span [nontrivial R]
   (hv : linear_independent R v) (f : ι' ↪ ι)
-  (hss : range v ⊆ span R (range (v ∘ f))) (zero_ne_one : 0 ≠ (1 : R)):
+  (hss : range v ⊆ span R (range (v ∘ f))) :
   surjective f :=
 begin
   intros i,
@@ -559,12 +561,12 @@ begin
   exact hi'.2
 end
 
-lemma eq_of_linear_independent_of_span_subtype {s t : set M} (zero_ne_one : (0 : R) ≠ 1)
+lemma eq_of_linear_independent_of_span_subtype [nontrivial R] {s t : set M}
   (hs : linear_independent R (λ x, x : s → M)) (h : t ⊆ s) (hst : s ⊆ span R t) : s = t :=
 begin
   let f : t ↪ s := ⟨λ x, ⟨x.1, h x.2⟩, λ a b hab, subtype.coe_injective (subtype.mk.inj hab)⟩,
   have h_surj : surjective f,
-  { apply surjective_of_linear_independent_of_span hs f _ zero_ne_one,
+  { apply surjective_of_linear_independent_of_span hs f _,
     convert hst; simp [f, comp], },
   show s = t,
   { apply subset.antisymm _ h,
@@ -622,13 +624,14 @@ lemma linear_independent_inl_union_inr' {v : ι → M} {v' : ι' → M'}
 begin
   by_cases zero_eq_one : (0 : R) = 1,
   { apply linear_independent_of_zero_eq_one zero_eq_one },
-  have inj_v : injective v := (linear_independent.injective zero_eq_one hv),
-  have inj_v' : injective v' := (linear_independent.injective zero_eq_one hv'),
+  haveI : nontrivial R := ⟨⟨0, 1, zero_eq_one⟩⟩,
+  have inj_v : injective v := (linear_independent.injective hv),
+  have inj_v' : injective v' := (linear_independent.injective hv'),
   apply linear_independent.of_subtype_range,
   { apply sum.elim_injective,
     { exact inl_injective.comp inj_v },
     { exact inr_injective.comp inj_v' },
-    { intros, simp [hv.ne_zero zero_eq_one] } },
+    { intros, simp [hv.ne_zero] } },
   { rw sum.elim_range,
     refine (hv.image _).to_subtype_range.union (hv'.image _).to_subtype_range _;
       [simp, simp, skip],
@@ -703,21 +706,21 @@ have h4 : g a = 0, from calc
 -- Now we're done; the last two facts together imply that `g` vanishes on every element of `insert a s`.
 (finset.forall_mem_insert _ _ _).2 ⟨h4, h3⟩)
 
-lemma le_of_span_le_span {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
+lemma le_of_span_le_span [nontrivial R] {s t u: set M}
   (hl : linear_independent R (coe : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u)
   (hst : span R s ≤ span R t) : s ⊆ t :=
 begin
-  have := eq_of_linear_independent_of_span_subtype zero_ne_one
+  have := eq_of_linear_independent_of_span_subtype
     (hl.mono (set.union_subset hsu htu))
     (set.subset_union_right _ _)
     (set.union_subset (set.subset.trans subset_span hst) subset_span),
   rw ← this, apply set.subset_union_left
 end
 
-lemma span_le_span_iff {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
+lemma span_le_span_iff [nontrivial R] {s t u: set M}
   (hl : linear_independent R (coe : u → M)) (hsu : s ⊆ u) (htu : t ⊆ u) :
   span R s ≤ span R t ↔ s ⊆ t :=
-⟨le_of_span_le_span zero_ne_one hl hsu htu, span_mono⟩
+⟨le_of_span_le_span hl hsu htu, span_mono⟩
 
 variables (R) (v)
 /-- A family of vectors is a basis if it is linearly independent and all vectors are in the span. -/
@@ -737,8 +740,8 @@ begin
   { rw[set.range_comp, range_iff_surjective.2 hf.2, image_univ, hv.2] }
 end
 
-lemma is_basis.injective (hv : is_basis R v) (zero_ne_one : (0 : R) ≠ 1) : injective v :=
-  λ x y h, linear_independent.injective zero_ne_one hv.1 h
+lemma is_basis.injective [nontrivial R] (hv : is_basis R v) : injective v :=
+  λ x y h, linear_independent.injective hv.1 h
 
 lemma is_basis.range (hv : is_basis R v) : is_basis R (λ x, x : range v → M) :=
 ⟨hv.1.to_subtype_range, by { convert hv.2, ext i, exact ⟨λ ⟨p, hp⟩, hp ▸ p.2, λ hi, ⟨⟨i, hi⟩, rfl⟩⟩ }⟩
@@ -1082,7 +1085,7 @@ lemma exists_sum_is_basis (hs : linear_independent K v) :
 begin
   -- This is a hack: we jump through hoops to reuse `exists_subset_is_basis`.
   let s := set.range v,
-  let e : ι ≃ s := equiv.set.range v (hs.injective zero_ne_one),
+  let e : ι ≃ s := equiv.set.range v hs.injective,
   have : (λ x, x : s → V) = v ∘ e.symm := by { funext, dsimp, rw [equiv.set.apply_range_symm v], },
   have : linear_independent K (λ x, x : s → V),
   { rw this,
@@ -1113,7 +1116,7 @@ have ∀t, ∀(s' : finset V), ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ (span
 assume t, finset.induction_on t
   (assume s' hs' _ hss',
     have s = ↑s',
-      from eq_of_linear_independent_of_span_subtype zero_ne_one hs hs' $
+      from eq_of_linear_independent_of_span_subtype hs hs' $
           by simpa using hss',
     ⟨s', by simp [this]⟩)
   (assume b₁ t hb₁t ih s' hs' hst hss',

src/linear_algebra/dimension.lean

@@ -53,7 +53,7 @@ theorem is_basis.le_span {v : ι → V} {J : set V} (hv : is_basis K v)
    (hJ : span K J = ⊤) : cardinal.mk (range v) ≤ cardinal.mk J :=
 begin
   cases le_or_lt cardinal.omega (cardinal.mk J) with oJ oJ,
-  { have := cardinal.mk_range_eq_of_injective (linear_independent.injective zero_ne_one hv.1),
+  { have := cardinal.mk_range_eq_of_injective (linear_independent.injective hv.1),
     let S : J → set ι := λ j, ↑(is_basis.repr hv j).support,
     let S' : J → set V := λ j, v '' S j,
     have hs : range v ⊆ ⋃ j, S' j,
@@ -94,14 +94,14 @@ begin
   apply le_antisymm,
   { convert cardinal.lift_le.{u' (max w w')}.2 (hv.le_span hv'.2),
     { rw cardinal.lift_max.{w u' w'},
-      apply (cardinal.mk_range_eq_of_injective (hv.injective zero_ne_one)).symm, },
+      apply (cardinal.mk_range_eq_of_injective hv.injective).symm, },
     { rw cardinal.lift_max.{w' u' w},
-      apply (cardinal.mk_range_eq_of_injective (hv'.injective zero_ne_one)).symm, }, },
+      apply (cardinal.mk_range_eq_of_injective hv'.injective).symm, }, },
   { convert cardinal.lift_le.{u' (max w w')}.2 (hv'.le_span hv.2),
     { rw cardinal.lift_max.{w' u' w},
-      apply (cardinal.mk_range_eq_of_injective (hv'.injective zero_ne_one)).symm, },
+      apply (cardinal.mk_range_eq_of_injective hv'.injective).symm, },
     { rw cardinal.lift_max.{w u' w'},
-      apply (cardinal.mk_range_eq_of_injective (hv.injective zero_ne_one)).symm, }, }
+      apply (cardinal.mk_range_eq_of_injective hv.injective).symm, }, }
 end
 
 theorem is_basis.mk_range_eq_dim {v : ι → V} (h : is_basis K v) :
@@ -111,13 +111,13 @@ begin
   rcases this with ⟨v', e⟩,
   rw e,
   apply cardinal.lift_inj.1,
-  rw cardinal.mk_range_eq_of_injective (h.injective zero_ne_one),
+  rw cardinal.mk_range_eq_of_injective h.injective,
   convert @mk_eq_mk_of_basis _ _ _ _ _ _ _ _ _ h v'.property
 end
 
 theorem is_basis.mk_eq_dim {v : ι → V} (h : is_basis K v) :
   cardinal.lift.{w u'} (cardinal.mk ι) = cardinal.lift.{u' w} (dim K V) :=
-by rw [←h.mk_range_eq_dim, cardinal.mk_range_eq_of_injective (h.injective zero_ne_one)]
+by rw [←h.mk_range_eq_dim, cardinal.mk_range_eq_of_injective h.injective]
 
 variables [add_comm_group V₂] [vector_space K V₂]
 
@@ -143,7 +143,7 @@ by rw [←cardinal.lift_inj, ← (@is_basis_singleton_one punit K _ _).mk_eq_dim
 lemma dim_span {v : ι → V} (hv : linear_independent K v) :
   dim K ↥(span K (range v)) = cardinal.mk (range v) :=
 by rw [←cardinal.lift_inj, ← (is_basis_span hv).mk_eq_dim,
-    cardinal.mk_range_eq_of_injective (@linear_independent.injective ι K V v _ _ _ zero_ne_one hv)]
+    cardinal.mk_range_eq_of_injective (@linear_independent.injective ι K V v _ _ _ _ hv)]
 
 lemma dim_span_set {s : set V} (hs : linear_independent K (λ x, x : s → V)) :
   dim K ↥(span K s) = cardinal.mk s :=

src/linear_algebra/finite_dimensional.lean

@@ -184,7 +184,7 @@ cardinality of the basis. -/
 lemma dim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
   dim K V = fintype.card ι :=
 by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
-       set.card_range_of_injective (h.injective zero_ne_one)]
+       set.card_range_of_injective h.injective]
 
 
 /-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the

src/linear_algebra/matrix.lean

@@ -213,15 +213,16 @@ theorem linear_equiv_matrix_range {ι κ M₁ M₂ : Type*}
     linear_equiv_matrix hv₁ hv₂ f k i :=
 if H : (0 : R) = 1 then eq_of_zero_eq_one H _ _ else
 begin
+  haveI : nontrivial R := ⟨⟨0, 1, H⟩⟩,
   simp_rw [linear_equiv_matrix, linear_equiv.trans_apply, linear_equiv_matrix'_apply,
-    ← equiv.of_injective_apply _ (hv₁.injective H), ← equiv.of_injective_apply _ (hv₂.injective H),
+    ← equiv.of_injective_apply _ hv₁.injective, ← equiv.of_injective_apply _ hv₂.injective,
     to_matrix_of_equiv, ← linear_equiv.trans_apply, linear_equiv.arrow_congr_trans], congr' 3;
   refine function.left_inverse.injective linear_equiv.symm_symm _; ext x;
   simp_rw [linear_equiv.symm_trans_apply, equiv_fun_basis_symm_apply, fun_congr_left_symm,
     fun_congr_left_apply, fun_left_apply],
-  convert (finset.sum_equiv (equiv.of_injective _ (hv₁.injective H)) _).symm,
+  convert (finset.sum_equiv (equiv.of_injective _ hv₁.injective) _).symm,
   simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk],
-  convert (finset.sum_equiv (equiv.of_injective _ (hv₂.injective H)) _).symm,
+  convert (finset.sum_equiv (equiv.of_injective _ hv₂.injective) _).symm,
   simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk]
 end
 
@@ -531,8 +532,9 @@ theorem trace_aux_range (R : Type u) [comm_ring R] {M : Type v} [add_comm_group
   trace_aux R hb.range = trace_aux R hb :=
 linear_map.ext $ λ f, if H : 0 = 1 then eq_of_zero_eq_one H _ _ else
 begin
+  haveI : nontrivial R := ⟨⟨0, 1, H⟩⟩,
   change ∑ i : set.range b, _ = ∑ i : ι, _, simp_rw [matrix.diag_apply], symmetry,
-  convert finset.sum_equiv (equiv.of_injective _ $ hb.injective H) _, ext i,
+  convert finset.sum_equiv (equiv.of_injective _ hb.injective) _, ext i,
   exact (linear_equiv_matrix_range hb hb f i i).symm
 end
 

src/ring_theory/noetherian.lean

@@ -351,7 +351,7 @@ begin
   have : ∀ a b : ℕ, a ≤ b ↔
     span R ((coe ∘ f) '' {m | m ≤ a}) ≤ span R ((coe ∘ f) '' {m | m ≤ b}),
   { assume a b,
-    rw [span_le_span_iff zero_ne_one hs (this a) (this b),
+    rw [span_le_span_iff hs (this a) (this b),
       set.image_subset_image_iff (subtype.coe_injective.comp f.injective),
       set.subset_def],
     exact ⟨λ hab x (hxa : x ≤ a), le_trans hxa hab, λ hx, hx a (le_refl a)⟩ },