From 5bb55bc72945d4a7a136b46a9ba6b75e3e3eb77c Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Tue, 17 Sep 2024 18:20:10 +0200 Subject: [PATCH] whitespace --- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean index a41ddc07fce46..2f8a1d3a28cd8 100644 --- a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean +++ b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean @@ -432,7 +432,7 @@ def logEmbeddingEquiv : @[simp] theorem logEmbeddingEquiv_apply (x : (𝓞 K)ˣ) : - logEmbeddingEquiv K (Additive.ofMul (QuotientGroup.mk x))= + logEmbeddingEquiv K (Additive.ofMul (QuotientGroup.mk x)) = logEmbedding K (Additive.ofMul x) := rfl instance : Module.Free ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=