Theorems · Theorem · linear algebra

Complex.liftAux_apply

∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) (z : ℂ),
  (Complex.liftAux I' hI') z = (algebraMap ℝ A) z.re + z.im • I'

Defined in

Mathlib.LinearAlgebra.Complex.Module

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAlgebra