isCommJordan

Mathlib.Algebra.Jordan.Basic

URI: https://scilib.ai/kg/mathlib#CommSemigroup.isCommJordan

English

If A is a commutative semigroup, then A is IsCommJordan.

Русский

Если A — коммутативная полугруппа, то A удовлетворяет IsCommJordan.

LaTeX

$$[CommSemigroup A] \Rightarrow IsCommJordan A$$

Lean4

instance (priority := 100) isCommJordan [CommSemigroup A] : IsCommJordan A where
  lmul_comm_rmul_rmul _ _ := mul_assoc _ _ _

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

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

Разделы

Аффилиация

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