Skip to content

Commit 6649421

Browse files
committed
chore(Data.Complex): add @[simp] to Complex.conj_ofReal (#14648)
This came up in #14601: it seems this `simp` lemma is missing, and as a consequence the `simp` set wouldn't converge. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Should.20docs.23Complex.2Econj_ofReal.20be.20.60.40.5Bsimp.5D.60.3F
1 parent 3cdee7b commit 6649421

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Mathlib/Data/Complex/Basic.lean

+1
Original file line numberDiff line numberDiff line change
@@ -560,6 +560,7 @@ theorem conj_im (z : ℂ) : (conj z).im = -z.im :=
560560
rfl
561561
#align complex.conj_im Complex.conj_im
562562

563+
@[simp]
563564
theorem conj_ofReal (r : ℝ) : conj (r : ℂ) = r :=
564565
ext_iff.2 <| by simp [star]
565566
#align complex.conj_of_real Complex.conj_ofReal

0 commit comments

Comments
 (0)