_aux_Mathlib_LinearAlgebra_Complex_Module___macroRules_ComplexStarModule_termℜ_1

English

The real part of I times a equals minus the imaginary part of a, i.e., Re(Ia) = -Im(a).

Русский

Действительная часть I∙a равна минус мнимая часть a: Re(Ia) = -Im(a).

LaTeX

$$$\\operatorname{realPart}(I a) = -\\operatorname{imaginaryPart}(a)$$$

Lean4

@[scoped macro ComplexStarModule.termℜ]
public meta def _aux_Mathlib_LinearAlgebra_Complex_Module___macroRules_ComplexStarModule_termℜ_1 : Macro✝ := fun
  | `(ℜ) => ``(realPart)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

Похожие утверждения