feat(algebra/punit_instances): linear_ordered_add_comm_monoid_with_to…

…p punit (#16609)
leanprover-community · Sep 23, 2022 · 27b9038 · 27b9038
1 parent 01894cc
commit 27b9038
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/algebra/punit_instances.lean b/src/algebra/punit_instances.lean
@@ -80,6 +80,11 @@ instance : linear_ordered_cancel_add_comm_monoid punit :=
 { le_of_add_le_add_left := λ _ _ _ _, trivial,
   .. punit.canonically_ordered_add_monoid, ..punit.linear_order }
 
+instance : linear_ordered_add_comm_monoid_with_top punit :=
+{ top_add' := λ _, rfl,
+  ..punit.complete_boolean_algebra,
+  ..punit.linear_ordered_cancel_add_comm_monoid }
+
 instance : has_smul R punit :=
 { smul := λ _ _, star }