Theorems · Theorem · linear algebra

realPart_smul

∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (z : ℂ) (a : A), realPart (z • a) = z.re • realPart a - z.im • imaginaryPart a

Defined in

Mathlib.LinearAlgebra.Complex.Module

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleStarAddMonoidStarModule