NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

remark.  [ca-0018]
✍️source

    The definition above (adopted in \(\textsf {Mathlib}\)) is more general than the definition in literature (e.g. [jadczyk2019notes, 1.6]):

    Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((M, *)\), satisfying:

    1. \(A\) is a module \(M\) over \(R\) under \(+\) and \(\bullet \).
    2. \(A\) is a ring under \(*\).
    3. For \(x, y \in A, a \in R\), we have
      4. \[ a \bullet (x * y) = (a \bullet x) * y = x * (a \bullet y) \]

    See Implementation notes in Algebra for details.