star_mul_star

Mathlib.Algebra.Star.Basic

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

English

For all x, y, star(x * star y) = y * star x.

Русский

Для всех x, y: star(x ⋅ star y) = y ⋅ star x.

LaTeX

$$$$ \star(x \cdot \star y) = y \cdot \star x. $$$$

Lean4

theorem star_mul_star (x y : R) : star (x * star y) = y * star x := by rw [star_mul, star_star]

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

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

Разделы

Аффилиация

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