feat(topology/instances/ereal): more on ereal, notably its topology (#…

…7765)
leanprover-community · Jun 8, 2021 · 5c6d3bc · 5c6d3bc
1 parent 75c81de
commit 5c6d3bc
Show file tree

Hide file tree

Showing 4 changed files with 723 additions and 21 deletions.
diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean
@@ -464,6 +464,10 @@ begin
     exact ⟨_, rfl, add_le_add_left h _⟩, }
 end
 
+instance [linear_ordered_add_comm_monoid α] : linear_ordered_add_comm_monoid (with_bot α) :=
+{ ..with_bot.linear_order,
+  ..with_bot.ordered_add_comm_monoid }
+
 -- `by norm_cast` proves this lemma, so I did not tag it with `norm_cast`
 lemma coe_zero [has_zero α] : ((0 : α) : with_bot α) = 0 := rfl