chore: backports for leanprover/lean4#4814 (part 24) (#15520)

Mathlib/Algebra/Module/LinearMap/Polynomial.lean

@@ -467,6 +467,7 @@ noncomputable
 def nilRank (φ : L →ₗ[R] Module.End R M) : ℕ :=
   nilRankAux φ (Module.Free.chooseBasis R L)
 
+section
 variable [Nontrivial R]
 
 lemma nilRank_eq_polyCharpoly_natTrailingDegree (b : Basis ι R L) :
@@ -480,7 +481,7 @@ lemma polyCharpoly_coeff_nilRank_ne_zero :
 
 open FiniteDimensional Module.Free
 
-lemma nilRank_le_card (b : Basis ι R M) : nilRank φ ≤ Fintype.card ι := by
+lemma nilRank_le_card {ι : Type*} [Fintype ι] (b : Basis ι R M) : nilRank φ ≤ Fintype.card ι := by
   apply Polynomial.natTrailingDegree_le_of_ne_zero
   rw [← FiniteDimensional.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
     Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]
@@ -498,6 +499,8 @@ lemma nilRank_le_natTrailingDegree_charpoly (x : L) :
   apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr _ h
   apply (LinearMap.charpoly_monic _).ne_zero
 
+end
+
 /-- Let `L` and `M` be finite free modules over `R`,
 and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms,
 and denote `n := nilRank φ`.
@@ -518,7 +521,7 @@ lemma isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero :
       ((polyCharpoly φ b).coeff (nilRank φ)) ≠ 0 := by
   rw [IsNilRegular, polyCharpoly_coeff_eval]
 
-lemma isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank :
+lemma isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank [Nontrivial R] :
     IsNilRegular φ x ↔ (φ x).charpoly.natTrailingDegree = nilRank φ := by
   rw [isNilRegular_def]
   constructor
@@ -535,7 +538,7 @@ section IsDomain
 
 variable [IsDomain R]
 
-open Cardinal FiniteDimensional MvPolynomial in
+open Cardinal FiniteDimensional MvPolynomial Module.Free in
 lemma exists_isNilRegular_of_finrank_le_card (h : finrank R M ≤ #R) :
     ∃ x : L, IsNilRegular φ x := by
   let b := chooseBasis R L

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -551,11 +551,11 @@ lemma nonsingular_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁)
     W.Nonsingular (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
   nonsingular_neg <| nonsingular_negAdd h₁ h₂ hxy
 
-variable {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂)
+variable {x₁ x₂ : F} (y₁ y₂ : F)
 
 /-- The formula x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²,
 where ψ(x,y) = 2y + a₁x + a₃. -/
-lemma addX_eq_addX_negY_sub :
+lemma addX_eq_addX_negY_sub (hx : x₁ ≠ x₂) :
     W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂))
       - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2 := by
   simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]
@@ -564,7 +564,7 @@ lemma addX_eq_addX_negY_sub :
 
 /-- The formula y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0,
 assuming that P₁ + P₂ + P₃ = O. -/
-lemma cyclic_sum_Y_mul_X_sub_X :
+lemma cyclic_sum_Y_mul_X_sub_X (hx : x₁ ≠ x₂) :
     letI x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)
     y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0 := by
   simp_rw [slope_of_X_ne hx, negAddY, addX]
@@ -574,7 +574,7 @@ lemma cyclic_sum_Y_mul_X_sub_X :
 /-- The formula
 ψ(P₁ + P₂) = (ψ(P₂)(x(P₁) - x(P₃)) - ψ(P₁)(x(P₂) - x(P₃))) / (x(P₂) - x(P₁)),
 where ψ(x,y) = 2y + a₁x + a₃. -/
-lemma addY_sub_negY_addY :
+lemma addY_sub_negY_addY (hx : x₁ ≠ x₂) :
     letI x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)
     letI y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)
     y₃ - W.negY x₃ y₃ =

Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean

@@ -92,7 +92,7 @@ theorem map_nhds_eq_of_surj [CompleteSpace E] [CompleteSpace F] {f : E → F} {f
   apply hs.map_nhds_eq f'symm s_nhds (Or.inr (NNReal.half_lt_self _))
   simp [ne_of_gt f'symm_pos]
 
-variable [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
+variable {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
 
 theorem approximates_deriv_on_open_nhds (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
     ∃ s : Set E, a ∈ s ∧ IsOpen s ∧
@@ -104,6 +104,7 @@ theorem approximates_deriv_on_open_nhds (hf : HasStrictFDerivAt f (f' : E →L[
       f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf'
 
 variable (f)
+variable [CompleteSpace E]
 
 /-- Given a function with an invertible strict derivative at `a`, returns a `PartialHomeomorph`
 with `to_fun = f` and `a ∈ source`. This is a part of the inverse function theorem.

Mathlib/Analysis/Convex/Body.lean

@@ -89,16 +89,23 @@ theorem zero_mem_of_symmetric (K : ConvexBody V) (h_symm : ∀ x ∈ K, - x ∈
 
 section ContinuousAdd
 
+instance : Zero (ConvexBody V) where
+  zero := ⟨0, convex_singleton 0, isCompact_singleton, Set.singleton_nonempty 0⟩
+
+@[simp] -- Porting note: add norm_cast; we leave it out for now to reproduce mathlib3 behavior.
+theorem coe_zero : (↑(0 : ConvexBody V) : Set V) = 0 :=
+  rfl
+
+instance : Inhabited (ConvexBody V) :=
+  ⟨0⟩
+
 variable [ContinuousAdd V]
 
 instance : Add (ConvexBody V) where
   add K L :=
     ⟨K + L, K.convex.add L.convex, K.isCompact.add L.isCompact,
       K.nonempty.add L.nonempty⟩
 
-instance : Zero (ConvexBody V) where
-  zero := ⟨0, convex_singleton 0, isCompact_singleton, Set.singleton_nonempty 0⟩
-
 instance : SMul ℕ (ConvexBody V) where
   smul := nsmulRec
 
@@ -114,13 +121,6 @@ instance : AddMonoid (ConvexBody V) :=
 theorem coe_add (K L : ConvexBody V) : (↑(K + L) : Set V) = (K : Set V) + L :=
   rfl
 
-@[simp] -- Porting note: add norm_cast; we leave it out for now to reproduce mathlib3 behavior.
-theorem coe_zero : (↑(0 : ConvexBody V) : Set V) = 0 :=
-  rfl
-
-instance : Inhabited (ConvexBody V) :=
-  ⟨0⟩
-
 instance : AddCommMonoid (ConvexBody V) :=
   SetLike.coe_injective.addCommMonoid (↑) rfl (fun _ _ ↦ rfl) fun _ _ ↦ coe_nsmul _ _
 

Mathlib/Analysis/Convex/GaugeRescale.lean

@@ -43,7 +43,21 @@ theorem gaugeRescale_smul (s t : Set E) {c : ℝ} (hc : 0 ≤ c) (x : E) :
   simp only [gaugeRescale, gauge_smul_of_nonneg hc, smul_smul, smul_eq_mul]
   rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]
 
-variable [TopologicalSpace E] [T1Space E]
+theorem gauge_gaugeRescale' (s : Set E) {t : Set E} {x : E} (hx : gauge t x ≠ 0) :
+    gauge t (gaugeRescale s t x) = gauge s x := by
+  rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
+    smul_eq_mul, div_mul_cancel₀ _ hx]
+
+theorem gauge_gaugeRescale_le (s t : Set E) (x : E) :
+    gauge t (gaugeRescale s t x) ≤ gauge s x := by
+  by_cases hx : gauge t x = 0
+  · simp [gaugeRescale, hx, gauge_nonneg]
+  · exact (gauge_gaugeRescale' s hx).le
+
+variable [TopologicalSpace E]
+
+section
+variable [T1Space E]
 
 theorem gaugeRescale_self_apply {s : Set E} (hsa : Absorbent ℝ s) (hsb : IsVonNBounded ℝ s)
     (x : E) : gaugeRescale s s x = x := by
@@ -55,23 +69,12 @@ theorem gaugeRescale_self {s : Set E} (hsa : Absorbent ℝ s) (hsb : IsVonNBound
     gaugeRescale s s = id :=
   funext <| gaugeRescale_self_apply hsa hsb
 
-theorem gauge_gaugeRescale' (s : Set E) {t : Set E} {x : E} (hx : gauge t x ≠ 0) :
-    gauge t (gaugeRescale s t x) = gauge s x := by
-  rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
-    smul_eq_mul, div_mul_cancel₀ _ hx]
-
 theorem gauge_gaugeRescale (s : Set E) {t : Set E} (hta : Absorbent ℝ t) (htb : IsVonNBounded ℝ t)
     (x : E) : gauge t (gaugeRescale s t x) = gauge s x := by
   rcases eq_or_ne x 0 with rfl | hx
   · simp
   · exact gauge_gaugeRescale' s ((gauge_pos hta htb).2 hx).ne'
 
-theorem gauge_gaugeRescale_le (s t : Set E) (x : E) :
-    gauge t (gaugeRescale s t x) ≤ gauge s x := by
-  by_cases hx : gauge t x = 0
-  · simp [gaugeRescale, hx, gauge_nonneg]
-  · exact (gauge_gaugeRescale' s hx).le
-
 theorem gaugeRescale_gaugeRescale {s t u : Set E} (hta : Absorbent ℝ t) (htb : IsVonNBounded ℝ t)
     (x : E) : gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x := by
   rcases eq_or_ne x 0 with rfl | hx; · simp
@@ -87,6 +90,8 @@ def gaugeRescaleEquiv (s t : Set E) (hsa : Absorbent ℝ s) (hsb : IsVonNBounded
   left_inv x := by rw [gaugeRescale_gaugeRescale, gaugeRescale_self_apply] <;> assumption
   right_inv x := by rw [gaugeRescale_gaugeRescale, gaugeRescale_self_apply] <;> assumption
 
+end
+
 variable [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s t : Set E}
 
 theorem mapsTo_gaugeRescale_interior (h₀ : t ∈ 𝓝 0) (hc : Convex ℝ t) :
@@ -100,6 +105,8 @@ theorem mapsTo_gaugeRescale_closure {s t : Set E} (hsc : Convex ℝ s) (hs₀ :
   mem_closure_of_gauge_le_one htc ht₀ hta <| (gauge_gaugeRescale_le _ _ _).trans <|
     (gauge_le_one_iff_mem_closure hsc hs₀).2 hx
 
+variable [T1Space E]
+
 theorem continuous_gaugeRescale {s t : Set E} (hs : Convex ℝ s) (hs₀ : s ∈ 𝓝 0)
     (ht : Convex ℝ t) (ht₀ : t ∈ 𝓝 0) (htb : IsVonNBounded ℝ t) :
     Continuous (gaugeRescale s t) := by

Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

@@ -218,15 +218,15 @@ end IsSelfAdjoint
 
 section FiniteDimensional
 
-variable [FiniteDimensional 𝕜 E] [_i : Nontrivial E] {T : E →ₗ[𝕜] E}
+variable [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E}
 
 namespace LinearMap
 
 namespace IsSymmetric
 
 /-- The supremum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial
 finite-dimensional vector space is an eigenvalue for that operator. -/
-theorem hasEigenvalue_iSup_of_finiteDimensional (hT : T.IsSymmetric) :
+theorem hasEigenvalue_iSup_of_finiteDimensional [Nontrivial E] (hT : T.IsSymmetric) :
     HasEigenvalue T ↑(⨆ x : { x : E // x ≠ 0 }, RCLike.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2 : ℝ) := by
   haveI := FiniteDimensional.proper_rclike 𝕜 E
   let T' := hT.toSelfAdjoint
@@ -245,7 +245,7 @@ theorem hasEigenvalue_iSup_of_finiteDimensional (hT : T.IsSymmetric) :
 
 /-- The infimum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial
 finite-dimensional vector space is an eigenvalue for that operator. -/
-theorem hasEigenvalue_iInf_of_finiteDimensional (hT : T.IsSymmetric) :
+theorem hasEigenvalue_iInf_of_finiteDimensional [Nontrivial E] (hT : T.IsSymmetric) :
     HasEigenvalue T ↑(⨅ x : { x : E // x ≠ 0 }, RCLike.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2 : ℝ) := by
   haveI := FiniteDimensional.proper_rclike 𝕜 E
   let T' := hT.toSelfAdjoint

Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean

@@ -74,7 +74,7 @@ end Ring
 section Field
 
 variable {R V : Type*} [Field R] [AddCommGroup V] [TopologicalSpace R] [TopologicalSpace V]
-  [TopologicalRing R] [TopologicalAddGroup V] [Module R V] [SeparatingDual R V]
+  [TopologicalRing R] [Module R V]
 
 -- TODO (@alreadydone): this could generalize to CommRing R if we were to add a section
 theorem _root_.separatingDual_iff_injective : SeparatingDual R V ↔
@@ -84,6 +84,8 @@ theorem _root_.separatingDual_iff_injective : SeparatingDual R V ↔
   rw [not_imp_comm, LinearMap.ext_iff]
   push_neg; rfl
 
+variable [SeparatingDual R V]
+
 open Function in
 /-- Given a finite-dimensional subspace `W` of a space `V` with separating dual, any
   linear functional on `W` extends to a continuous linear functional on `V`.
@@ -111,6 +113,8 @@ theorem exists_eq_one_ne_zero_of_ne_zero_pair {x y : V} (hx : x ≠ 0) (hy : y 
   · exact ⟨(v x)⁻¹ • v, inv_mul_cancel vx, show (v x)⁻¹ * v y ≠ 0 by simp [vx, vy]⟩
   · exact ⟨u + v, by simp [ux, vx], by simp [uy, vy]⟩
 
+variable [TopologicalAddGroup V]
+
 /-- In a topological vector space with separating dual, the group of continuous linear equivalences
 acts transitively on the set of nonzero vectors: given two nonzero vectors `x` and `y`, there
 exists `A : V ≃L[R] V` mapping `x` to `y`. -/

Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

@@ -536,8 +536,6 @@ end PresheafedSpace
 
 namespace SheafedSpace
 
-variable [HasProducts.{v} C]
-
 /-- A family of gluing data consists of
 1. An index type `J`
 2. A sheafed space `U i` for each `i : J`.

Mathlib/GroupTheory/PushoutI.lean

@@ -563,7 +563,8 @@ noncomputable def equiv : PushoutI φ ≃ NormalWord d :=
       simp only [prod_smul, prod_empty, mul_one]
     right_inv := fun w => prod_smul_empty w }
 
-theorem prod_injective : Function.Injective (prod : NormalWord d → PushoutI φ) := by
+theorem prod_injective {ι : Type*} {G : ι → Type*} [(i : ι) → Group (G i)] {φ : (i : ι) → H →* G i}
+    {d : Transversal φ} : Function.Injective (prod : NormalWord d → PushoutI φ) := by
   letI := Classical.decEq ι
   letI := fun i => Classical.decEq (G i)
   classical exact equiv.symm.injective
@@ -636,8 +637,8 @@ theorem Reduced.exists_normalWord_prod_eq (d : Transversal φ) {w : Word G} (hw
 /-- For any word `w` in the coproduct,
 if `w` is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then
 `w` itself is not in the image of the base group. -/
-theorem Reduced.eq_empty_of_mem_range (hφ : ∀ i, Injective (φ i))
-    {w : Word G} (hw : Reduced φ w)
+theorem Reduced.eq_empty_of_mem_range
+    (hφ : ∀ i, Injective (φ i)) {w : Word G} (hw : Reduced φ w)
     (h : ofCoprodI w.prod ∈ (base φ).range) : w = .empty := by
   rcases transversal_nonempty φ hφ with ⟨d⟩
   rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩
@@ -655,7 +656,8 @@ end Reduced
 
 /-- The intersection of the images of the maps from any two distinct groups in the diagram
 into the amalgamated product is the image of the map from the base group in the diagram. -/
-theorem inf_of_range_eq_base_range (hφ : ∀ i, Injective (φ i)) {i j : ι} (hij : i ≠ j) :
+theorem inf_of_range_eq_base_range
+    (hφ : ∀ i, Injective (φ i)) {i j : ι} (hij : i ≠ j) :
     (of i).range ⊓ (of j).range = (base φ).range :=
   le_antisymm
     (by

Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

@@ -290,6 +290,15 @@ lemma ker_restrict_eq_of_codisjoint {p q : Submodule R M} (hpq : Codisjoint p q)
   · ext ⟨x, hx⟩
     simpa using LinearMap.congr_fun h x
 
+lemma inf_orthogonal_self_le_ker_restrict {W : Submodule R M} (b₁ : B.IsRefl) :
+    W ⊓ B.orthogonal W ≤ (LinearMap.ker <| B.restrict W).map W.subtype := by
+  rintro v ⟨hv : v ∈ W, hv' : v ∈ B.orthogonal W⟩
+  simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coeSubtype, Subtype.exists,
+    exists_and_left, exists_prop, exists_eq_right_right]
+  refine ⟨?_, hv⟩
+  ext ⟨w, hw⟩
+  exact b₁ w v <| hv' w hw
+
 variable [FiniteDimensional K V]
 
 open FiniteDimensional Submodule
@@ -381,15 +390,6 @@ lemma orthogonal_eq_bot_iff
   rw [h, eq_bot_iff]
   exact fun x hx ↦ b₃ x fun y ↦ b₁ y x <| by simpa using hx y
 
-lemma inf_orthogonal_self_le_ker_restrict (b₁ : B.IsRefl) :
-    W ⊓ B.orthogonal W ≤ (LinearMap.ker <| B.restrict W).map W.subtype := by
-  rintro v ⟨hv : v ∈ W, hv' : v ∈ B.orthogonal W⟩
-  simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coeSubtype, Subtype.exists,
-    exists_and_left, exists_prop, exists_eq_right_right]
-  refine ⟨?_, hv⟩
-  ext ⟨w, hw⟩
-  exact b₁ w v <| hv' w hw
-
 end
 
 /-! We note that we cannot use `BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal` for the

Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -37,7 +37,7 @@ section CommSemiring
 variable [CommSemiring R] [CommSemiring A]
 variable [AddCommMonoid M₁] [AddCommMonoid M₂]
 variable [Algebra R A] [Module R M₁] [Module A M₁]
-variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁]
+variable [SMulCommClass R A M₁] [IsScalarTower R A M₁]
 variable [Module R M₂]
 
 variable (R A) in
@@ -99,7 +99,6 @@ variable [AddCommGroup M₁] [AddCommGroup M₂]
 variable [Module R M₁] [Module R M₂]
 variable [Module.Free R M₁] [Module.Finite R M₁]
 variable [Module.Free R M₂] [Module.Finite R M₂]
-variable [Nontrivial R]
 
 variable (R) in
 /-- `tensorDistrib` as an equivalence. -/

Mathlib/LinearAlgebra/Charpoly/Basic.lean

@@ -24,7 +24,7 @@ in any basis is in `LinearAlgebra/Charpoly/ToMatrix`.
 
 universe u v w
 
-variable {R : Type u} {M : Type v} [CommRing R] [Nontrivial R]
+variable {R : Type u} {M : Type v} [CommRing R]
 variable [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
 
 open Matrix Polynomial
@@ -52,7 +52,8 @@ theorem charpoly_monic : f.charpoly.Monic :=
   Matrix.charpoly_monic _
 
 open FiniteDimensional in
-lemma charpoly_natDegree [StrongRankCondition R] : natDegree (charpoly f) = finrank R M := by
+lemma charpoly_natDegree [Nontrivial R] [StrongRankCondition R] :
+    natDegree (charpoly f) = finrank R M := by
   rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]
 
 end Coeff
@@ -88,7 +89,7 @@ theorem pow_eq_aeval_mod_charpoly (k : ℕ) : f ^ k = aeval f (X ^ k %ₘ f.char
 
 variable {f}
 
-theorem minpoly_coeff_zero_of_injective (hf : Function.Injective f) :
+theorem minpoly_coeff_zero_of_injective [Nontrivial R] (hf : Function.Injective f) :
     (minpoly R f).coeff 0 ≠ 0 := by
   intro h
   obtain ⟨P, hP⟩ := X_dvd_iff.2 h

Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

@@ -32,7 +32,7 @@ We show the additional results:
 
 variable {R A V : Type*}
 variable [CommRing R] [CommRing A] [AddCommGroup V]
-variable [Algebra R A] [Module R V] [Module A V] [IsScalarTower R A V]
+variable [Algebra R A] [Module R V]
 variable [Invertible (2 : R)]
 
 open scoped TensorProduct

Mathlib/LinearAlgebra/Contraction.lean

@@ -201,7 +201,7 @@ section CommRing
 variable [CommRing R]
 variable [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q]
 variable [Module R M] [Module R N] [Module R P] [Module R Q]
-variable [Free R M] [Finite R M] [Free R N] [Finite R N] [Nontrivial R]
+variable [Free R M] [Finite R M] [Free R N] [Finite R N]
 
 /-- When `M` is a finite free module, the map `lTensorHomToHomLTensor` is an equivalence. Note
 that `lTensorHomEquivHomLTensor` is not defined directly in terms of