Skip to content

Commit

Permalink
chore: two cdots to cdots
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed May 10, 2024
1 parent c052670 commit 041b63e
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/DualNumber.lean
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ theorem lift_inlAlgHom_eps :
/-- Show DualNumber with values x and y as an "x + y*ε" string -/
instance instRepr [Repr R] : Repr (DualNumber R) where
reprPrec f p :=
(if p > 65 then (Std.Format.bracket "(" . ")") else (·)) <|
(if p > 65 then (Std.Format.bracket "(" · ")") else (·)) <|
reprPrec f.fst 65 ++ " + " ++ reprPrec f.snd 70 ++ "*ε"

end DualNumber
2 changes: 1 addition & 1 deletion Mathlib/Data/Complex/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -951,7 +951,7 @@ numbers are represented.
-/
unsafe instance instRepr : Repr ℂ where
reprPrec f p :=
(if p > 65 then (Std.Format.bracket "(" . ")") else (·)) <|
(if p > 65 then (Std.Format.bracket "(" · ")") else (·)) <|
reprPrec f.re 65 ++ " + " ++ reprPrec f.im 70 ++ "*I"

end Complex
Expand Down

0 comments on commit 041b63e

Please sign in to comment.