Theorems · Definition · linear algebra

Complex.liftAux

{A : Type u_1} → [inst : Ring A] → [inst_1 : Algebra ℝ A] → (I' : A) → I' * I' = -1 → ℂ →ₐ[ℝ] A

There is an AlgHom from ℂ to any ℝ-algebra with an element that squares to -1. See Complex.lift for this as an equiv.

Defined in

Mathlib.LinearAlgebra.Complex.Module

Cited by

7 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAlgebra