Theorem LinearOrderedAddCommGroupWithTop.add_eq_top

Modification history

2025-12-17 18:54

Mathlib/Algebra/Order/AddGroupWithTop.lean

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

Modified LinearOrderedAddCommGroupWithTop.add_eq_top View on Github →

2024-11-06 04:34

Mathlib/Algebra/Order/AddGroupWithTop.lean

feat: SubtractionMonoid instance for LinearOrderedAddCommGroupWithTop (#18665)

Added LinearOrderedAddCommGroupWithTop.add_eq_top View on Github →