termℑ

Mathlib.LinearAlgebra.Complex.Module

URI: https://scilib.ai/kg/mathlib#ComplexStarModule.termℑ

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[inherit_doc imaginaryPart, scoped term_parser 1000]
public meta def termℑ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ComplexStarModule.termℑ 1024 (ParserDescr.symbol✝ "ℑ")

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru