mul_star_self_pos

Mathlib.Algebra.Order.Star.Basic

URI: https://scilib.ai/kg/mathlib#mul_star_self_pos

English

If x is nonzero and the ring is nontrivial, then x star x is positive.

Русский

Если x не ноль и кольцо несубк, то x ⋅ x^* положительно.

LaTeX

$$$ 0 < x \cdot x^* $$$

Lean4

theorem mul_star_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < x * star x := by
  simpa using star_mul_self_pos hx.star

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

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

Разделы

Аффилиация

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