Theorem Positive.val_one

Modification history

2024-07-16 22:43
Mathlib/Algebra/Order/Positive/Ring.lean
chore (Algebra.Order.Ring.Defs): split file and unbundle results (#14393) …
Modified Positive.val_oneView on Github →
2022-12-09 01:07
Mathlib/Algebra/Order/Positive/Ring.lean
feat port:Algebra.Order.Positive.Ring (#911) …
Added Positive.val_oneView on Github →