From f7c20d3898b93b1ee7872c28069d2291671ecc8e Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 9 Dec 2024 12:01:55 +0000 Subject: [PATCH] chore: add issue number --- FLT/Mathlib/RingTheory/Norm/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FLT/Mathlib/RingTheory/Norm/Defs.lean b/FLT/Mathlib/RingTheory/Norm/Defs.lean index d7beab76..86101275 100644 --- a/FLT/Mathlib/RingTheory/Norm/Defs.lean +++ b/FLT/Mathlib/RingTheory/Norm/Defs.lean @@ -7,4 +7,4 @@ variable {M A B : Type*} [CommRing A] [CommRing B] [AddCommGroup M] [Algebra A B -- for free modules of finite rank lemma det_restrictScalars (f : M →ₗ[B] M) : (f.restrictScalars A).det = Algebra.norm A f.det := by - sorry + sorry -- #275