feat(analysis/normed_space/star and data/complex/is_R_or_C): register…

… instances of `cstar_ring` (#10555) Register instances `cstar_ring ℝ` and `cstar_ring K` when `[is_R_or_C K]`
leanprover-community · Dec 1, 2021 · 599a511 · 599a511
1 parent 3f7d0cf
commit 599a511
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/analysis/normed_space/star.lean b/src/analysis/normed_space/star.lean
@@ -42,6 +42,9 @@ for every `x`. -/
 class cstar_ring (E : Type*) [normed_ring E] [star_ring E] :=
 (norm_star_mul_self : ∀ {x : E}, ∥x⋆ * x∥ = ∥x∥ * ∥x∥)
 
+noncomputable instance : cstar_ring ℝ :=
+{ norm_star_mul_self := λ x, by simp only [star, id.def, normed_field.norm_mul] }
+
 variables {𝕜 E : Type*}
 
 open cstar_ring

diff --git a/src/data/complex/is_R_or_C.lean b/src/data/complex/is_R_or_C.lean
@@ -6,6 +6,7 @@ Authors: Frédéric Dupuis
 import data.real.sqrt
 import field_theory.tower
 import analysis.normed_space.finite_dimension
+import analysis.normed_space.star
 
 /-!
 # `is_R_or_C`: a typeclass for ℝ or ℂ
@@ -355,6 +356,9 @@ by field_simp
 lemma norm_conj {z : K} : ∥conj z∥ = ∥z∥ :=
 by simp only [←sqrt_norm_sq_eq_norm, norm_sq_conj]
 
+@[priority 100] instance : cstar_ring K :=
+{ norm_star_mul_self := λ x, (normed_field.norm_mul _ _).trans $ congr_arg (* ∥x∥) norm_conj }
+
 /-! ### Cast lemmas -/
 
 @[simp, norm_cast, priority 900] theorem of_real_nat_cast (n : ℕ) : ((n : ℝ) : K) = n :=