From b68131b4eb9eaef9f320b5d1c0da88071f53f201 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 19 Nov 2024 11:25:01 +0100 Subject: [PATCH] why not --- FltRegular/NumberTheory/IdealNorm.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean index ceaa512c..0f48c27c 100644 --- a/FltRegular/NumberTheory/IdealNorm.lean +++ b/FltRegular/NumberTheory/IdealNorm.lean @@ -233,7 +233,6 @@ variable [Module.Finite R S] [IsDedekindDomain R] [IsDedekindDomain S] /-- Multiplicativity of `Ideal.spanIntNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/ theorem spanIntNorm_mul [Module.Free R S] (I J : Ideal S) : spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J := by - classical nontriviality R cases subsingleton_or_nontrivial S · have : ∀ I : Ideal S, I = ⊤ := fun I ↦ Subsingleton.elim I ⊤