liftAux_apply_I

Mathlib.LinearAlgebra.Complex.Module

URI: https://scilib.ai/kg/mathlib#Complex.liftAux_apply_I

English

For any I' ∈ A, if hI' holds, then liftAux(I', hI') applied to I (the imaginary unit) equals I'.

Русский

Если на элемент I' из A выполняется условие hI', то liftAux(I', hI')(i) = I'.

LaTeX

$$$ liftAux(I',hI') (\\mathbb{i}) = I'. $$$

Lean4

theorem liftAux_apply_I (I' : A) (hI') : liftAux I' hI' I = I' := by simp

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

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

Разделы

Аффилиация

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