Theorem Positive.val_mul

Modification history

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