From 02fef3c856d41f4cff39b1b14eb2985d1decc89e Mon Sep 17 00:00:00 2001 From: riccardobrasca Date: Mon, 27 Nov 2023 18:51:14 +0100 Subject: [PATCH] fix build --- FltRegular/NumberTheory/KummersLemma/KummersLemma.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean index a89c1ed3..7e4f7ecb 100644 --- a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean +++ b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean @@ -64,6 +64,9 @@ theorem exists_units_eq_div_root_of_isUnramified rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A K L] exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _) rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hAB + letI : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra _ _ + have : IsScalarTower A (FractionRing A) (FractionRing B) := + FractionRing.isScalarTower_liftAlgebra _ _ have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B)) ↑(FractionRing.algEquiv A K).symm.toRingEquiv = RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L)