isJordan — Mathlib

English

A semigroup multiplication satisfies the (non-commutative) Jordan axioms.

Русский

Умножение в полугруппе удовлетворяет некоммутативным аксиомам Джордана.

LaTeX

$$IsJordan A for [Semigroup A]$$

Lean4

/-- Semigroup multiplication satisfies the (non-commutative) Jordan axioms -/
instance (priority := 100) isJordan [Semigroup A] : IsJordan A
    where
  lmul_comm_rmul a b := by rw [mul_assoc]
  lmul_lmul_comm_lmul a b := by rw [mul_assoc, mul_assoc]
  lmul_comm_rmul_rmul a b := by rw [mul_assoc]
  lmul_lmul_comm_rmul a b := by rw [← mul_assoc]
  rmul_comm_rmul_rmul a
    b := by
    rw [← mul_assoc, ← mul_assoc]
      -- see Note [lower instance priority]

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