From 3207195a201e99a5009fa0d6a2af79e21012de40 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 29 Oct 2024 12:21:06 +0100 Subject: [PATCH] minigolf --- FltRegular/NumberTheory/Hilbert92.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index e5e21f7b..c08752ea 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -600,7 +600,7 @@ lemma relativeUnitsModule_zeta_smul (x) : addMonoidEndRingEquivInt_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, addMonoidHomLequivInt_apply, Module.AEval.of_symm_smul, Polynomial.aeval_X, LinearEquiv.symm_apply_apply, LinearMap.smul_def, AddMonoidHom.coe_toIntLinearMap, - MonoidHom.toAdditive_apply_apply, toMul_ofMul, relativeUnitsMap_mk, unit_to_U] + MonoidHom.toAdditive_apply_apply, toMul_ofMul, unit_to_U] rfl local instance {M} [AddCommGroup M] : NoZeroSMulDivisors ℤ (M ⧸ AddCommGroup.torsion M) := by