Commit 2022-12-09 01:07 a388280c

View on Github →

feat port:Algebra.Order.Positive.Ring (#911) 655994e298904d7e5bbd1e18c95defd7b543eb94 Renaming coe_mul etc to val_mul and giving names to instances the only real changes here.

Estimated changes

added theorem Positive.coe_add
added theorem Positive.val_mul
added theorem Positive.val_one
added theorem Positive.val_pow