mul_star_self_ne_zero_iff

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#CStarRing.mul_star_self_ne_zero_iff

English

In a C*-algebra with a star operation, for every element x, x x* ≠ 0 if and only if x ≠ 0.

Русский

В C*-алгебре с операцией звезды для любого элемента x выполняется x x* ≠ 0 тогда и только тогда, когда x ≠ 0.

LaTeX

$$$ x x^{\star} \neq 0 \iff x \neq 0 $$$

Lean4

theorem mul_star_self_ne_zero_iff (x : E) : x * x⋆ ≠ 0 ↔ x ≠ 0 := by simp only [Ne, mul_star_self_eq_zero_iff]

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

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

Разделы

Аффилиация

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