imaginaryPart_imaginaryPart

Mathlib.LinearAlgebra.Complex.Module

URI: https://scilib.ai/kg/mathlib#imaginaryPart_imaginaryPart

English

The imaginary part of the imaginary part vanishes: Im(Im(x)) = 0.

Русский

Мнимая часть мнимая часть равна нулю: Im(Im(x)) = 0.

LaTeX

$$$\\operatorname{imaginaryPart}(\\operatorname{imaginaryPart}(x)) = 0$$$

Lean4

theorem imaginaryPart_imaginaryPart {x : A} : ℑ (ℑ x : A) = 0 :=
  (ℑ x).property.imaginaryPart

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

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

Разделы

Аффилиация

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