star

Mathlib.Algebra.Star.Basic

URI: https://scilib.ai/kg/mathlib#IsRegular.star

English

IsRegular is preserved under star: IsRegular(star x) iff IsRegular x.

Русский

IsRegular сохраняется под star: IsRegular(star x) эквивалентно IsRegular x.

LaTeX

$$$\text{IsRegular}(\star x) \iff \text{IsRegular}(x).$$$

Lean4

protected theorem star [Mul R] [StarMul R] {x : R} (hx : IsRegular x) : IsRegular (star x) :=
  ⟨hx.right.star, hx.left.star⟩

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

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

Разделы

Аффилиация

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