Homotopy Type Theory commutative ring > history (changes)

Showing changes from revision #11 to #12: Added | Removed | Changed

Definition

< commutative ring

A

commutative ring is a ring (A,+,,0,,1)(A, +, -, 0, \cdot, 1) with

  • a commutative identity for \cdot
    m κ: (a:A) (b:A)ab=bam_\kappa:\prod_{(a:A)} \prod_{(b:A)} a\cdot b = b\cdot a

Examples

See also

References

  • Frank Quinn?, Proof Projects for Teachers (pdf)

Last revised on June 17, 2022 at 20:31:11. See the history of this page for a list of all contributions to it.