instNonAssocRingOfInvertibleOfNat

English

The symmetrization αˢʸᵐ of a ring α with invertible 2 is a non-associative ring.

Русский

Симметризование αˢʸᵐ кольца α с обратимостью 2 образует неассоциированное кольцо.

LaTeX

$$$\alpha^{\mathrm{sym}} \text{ is a non-associative ring}$$$

Lean4

/-- The symmetrization of a real (unital, associative) algebra is a non-associative ring. -/
instance [Ring α] [Invertible (2 : α)] : NonAssocRing αˢʸᵐ :=
  { SymAlg.nonAssocSemiring, SymAlg.addCommGroup with }

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