star_def

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.star_def

English

The star operation on the field coincides with complex conjugation.

Русский

Операция звезды на поле совпадает с комплексным сопряжением.

LaTeX

$$$$\\text{Star}(z) = \\overline{z} \\quad\\text{for all } z.$$$$

Lean4

@[simp]
theorem star_def : (Star.star : K → K) = conj :=
  rfl

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

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

Разделы

Аффилиация

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