Skip to content

Commit e81c1a4

Browse files
committed
feat(UnitDisc/Basic): add two missing simp lemmas (leanprover-community#34430)
1 parent 8c557f9 commit e81c1a4

1 file changed

Lines changed: 3 additions & 0 deletions

File tree

Mathlib/Analysis/Complex/UnitDisc/Basic.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,9 @@ theorem re_neg (z : 𝔻) : (-z).re = -z.re :=
242242
theorem im_neg (z : 𝔻) : (-z).im = -z.im :=
243243
rfl
244244

245+
@[simp] theorem re_zero : re 0 = 0 := rfl
246+
@[simp] theorem im_zero : im 0 = 0 := rfl
247+
245248
/-- Conjugate point of the unit disc. -/
246249
instance : Star 𝔻 where
247250
star z := mk (conj z) <| (norm_conj z).symm ▸ z.norm_lt_one

0 commit comments

Comments
 (0)