feat(analysis/normed_space): normed_group punit (#7616)

Minor content from LTE.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/analysis/normed_space/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
+import algebra.punit_instances
 import topology.instances.nnreal
 import topology.algebra.module
 import topology.algebra.algebra
@@ -86,6 +87,12 @@ noncomputable def semi_normed_group.of_core (α : Type*) [add_comm_group α] [ha
     calc ∥x - y∥ = ∥ -(y - x)∥ : by simp
              ... = ∥y - x∥ : by { rw [C.norm_neg] } }
 
+instance : normed_group punit :=
+{ norm := function.const _ 0,
+  dist_eq := λ _ _, rfl, }
+
+@[simp] lemma punit.norm_eq_zero (r : punit) : ∥r∥ = 0 := rfl
+
 instance : normed_group ℝ :=
 { norm := λ x, abs x,
   dist_eq := assume x y, rfl }
@@ -773,6 +780,11 @@ class normed_comm_ring (α : Type*) extends normed_ring α :=
 instance normed_comm_ring.to_semi_normed_comm_ring [β : normed_comm_ring α] :
   semi_normed_comm_ring α := { ..β }
 
+instance : normed_comm_ring punit :=
+{ norm_mul := λ _ _, by simp,
+  ..punit.normed_group,
+  ..punit.comm_ring, }
+
 /-- A mixin class with the axiom `∥1∥ = 1`. Many `normed_ring`s and all `normed_field`s satisfy this
 axiom. -/
 class norm_one_class (α : Type*) [has_norm α] [has_one α] : Prop :=

src/topology/metric_space/basic.lean

@@ -1876,6 +1876,20 @@ metric_space.induced coe (λ x y, subtype.ext) t
 
 theorem subtype.dist_eq {p : α → Prop} (x y : subtype p) : dist x y = dist (x : α) y := rfl
 
+instance : metric_space empty :=
+{ dist := λ _ _, 0,
+  dist_self := λ _, rfl,
+  dist_comm := λ _ _, rfl,
+  eq_of_dist_eq_zero := λ _ _ _, subsingleton.elim _ _,
+  dist_triangle := λ _ _ _, show (0:ℝ) ≤ 0 + 0, by rw add_zero, }
+
+instance : metric_space punit :=
+{ dist := λ _ _, 0,
+  dist_self := λ _, rfl,
+  dist_comm := λ _ _, rfl,
+  eq_of_dist_eq_zero := λ _ _ _, subsingleton.elim _ _,
+  dist_triangle := λ _ _ _, show (0:ℝ) ≤ 0 + 0, by rw add_zero, }
+
 section real
 
 /-- Instantiate the reals as a metric space. -/

src/topology/uniform_space/basic.lean

@@ -1089,7 +1089,7 @@ lemma to_topological_space_inf {u v : uniform_space α} :
 by rw [to_topological_space_Inf, infi_pair]
 
 instance : uniform_space empty := ⊥
-instance : uniform_space unit := ⊥
+instance : uniform_space punit := ⊥
 instance : uniform_space bool := ⊥
 instance : uniform_space ℕ := ⊥
 instance : uniform_space ℤ := ⊥