conjAe_coe

Mathlib.LinearAlgebra.Complex.Module

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

English

The function conj equals the underlying function of conjAe.

Русский

Функция сопряжения совпадает с базовой функцией conjAe.

LaTeX

$$$ \text{ The underlying function of } conjAe \text{ is } conj. $$$

Lean4

@[simp]
theorem conjAe_coe : ⇑conjAe = conj :=
  rfl

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

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

Разделы

Аффилиация

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