Homotopy Type Theory commutative ring > history (Rev #10, changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

Definition

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)

Revision on June 16, 2022 at 16:55:15 by Anonymous?. See the history of this page for a list of all contributions to it.