x y : ℂ
⊢ ↑(starRingEnd ℂ) (exp x + exp (-x)) / 2 = ↑(starRingEnd ℂ) (exp x + exp (-x)) / ↑(starRingEnd ℂ) 2
x y : ℂ
⊢ cosh (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (cosh x)
rw [cosh, ← RingHom.map_neg, exp_conj, exp_conj, ← RingHom.map_add, cosh, map_div₀]
no goals
x y : ℂ
⊢ ↑(starRingEnd ℂ) (exp x + exp (-x)) / 2 = ↑(starRingEnd ℂ) (exp x + exp (-x)) / ↑(starRingEnd ℂ) 2
simp [← one_add_one_eq_two]