Theorem LinearOrderedAddCommGroupWithTop.isAddUnit_iff

Modification history

2025-12-17 18:54
Mathlib/Algebra/Order/AddGroupWithTop.lean
chore(Algebra/Order/AddGroupWithTop): golf (#32382)
Added LinearOrderedAddCommGroupWithTop.isAddUnit_iffView on Github →