Theorem Positive.coe_add

Modification history

2022-12-09 01:07
Mathlib/Algebra/Order/Positive/Ring.lean
feat port:Algebra.Order.Positive.Ring (#911) …
Added Positive.coe_addView on Github →