Theorem LinearOrderedAddCommGroupWithTop.top_ne_zero

Modification history

2025-12-17 18:54

Mathlib/Algebra/Order/AddGroupWithTop.lean

chore(Algebra/Order/AddGroupWithTop): golf (#32382)

Modified LinearOrderedAddCommGroupWithTop.top_ne_zero View on Github →

2024-11-06 04:34

Mathlib/Algebra/Order/AddGroupWithTop.lean

feat: SubtractionMonoid instance for LinearOrderedAddCommGroupWithTop (#18665)

Added LinearOrderedAddCommGroupWithTop.top_ne_zero View on Github →