conjugate_nonneg'

Mathlib.Algebra.Order.Star.Basic

URI: https://scilib.ai/kg/mathlib#conjugate_nonneg'

← MathLib Explorer

English

If a ≥ 0, then for any c, star c · a · star c ≥ 0.

Русский

Если a ≥ 0, то для любого c, star c · a · star c ≥ 0.

LaTeX

$$$0 \le a \Rightarrow 0 \le \star c \cdot a \cdot \star c$$$

Lean4

@[aesop safe apply]
theorem conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c := by
  simpa only [star_star] using conjugate_nonneg ha (star c)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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