whitespace

leanprover-community · Sep 17, 2024 · 5bb55bc · 5bb55bc
1 parent fe7db50
commit 5bb55bc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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))) :=