Skip to content

Commit

Permalink
chore: two dots to cdots (#12808)
Browse files Browse the repository at this point in the history
Replace two `.` with `·`.

Found by the linter at #12143.
  • Loading branch information
adomani committed May 11, 2024
1 parent 3be9527 commit d8189c0
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 d8189c0

Please sign in to comment.