Zulip Chat Archive
Stream: Is there code for X?
Topic: The canonical `ℂ →ₐ[ℝ] A` given a square root of -1
Eric Wieser (Jun 28 2021 at 12:16):
Do we have:
def complex.lift {A : Type*} [ring A] [algebra ℝ A] (I' : A) (hI' : I' * I' = -1) : ℂ →ₐ[ℝ] A := sorry
which sends complex.I to I'?
Last updated: May 02 2025 at 03:31 UTC