I_im'

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.I_im'

English

Im(I) times Im(z) equals Im(z) for all z.

Русский

Мнимая часть I умножается на мнимаю часть z, давая мнимую часть z.

LaTeX

$$$\operatorname{Im}(I) \cdot \operatorname{Im}(z) = \operatorname{Im}(z)$$$

Lean4

@[simp, rclike_simps]
theorem I_im' (z : K) : im (I : K) * im z = im z := by
  rw [mul_comm, I_im]
    -- Not `@[simp]` since `simp` can prove this.

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

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

Разделы

Аффилиация

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