oops

leanprover-community · Oct 31, 2024 · 238a276 · 238a276
1 parent 46afabc
commit 238a276
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean
@@ -1379,4 +1379,3 @@ lemma RingHom.surjective_of_tmul_eq_tmul_of_finite {R S}
       have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R S)⟩
       rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
   cases false_of_nontrivial_of_subsingleton ((S ⧸ R') ⊗[R] (S ⧸ R'))
-#min_imports