From cac9242e10112eb971b4084f47852afd9bb7889e Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 4 Mar 2022 14:03:53 +0000 Subject: [PATCH] chore(analysis/complex/basic): golf `norm_rat/int/int_of_nonneg` (#12433) While looking at PR #12428, I found some easy golfing of some lemmas (featuring my first-ever use of `single_pass`! :smile: ). --- src/analysis/complex/basic.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean index bc63adf079a60..b27b62e81faa4 100644 --- a/src/analysis/complex/basic.lean +++ b/src/analysis/complex/basic.lean @@ -76,17 +76,15 @@ by rw [dist_comm, dist_self_conj] @[simp] lemma norm_real (r : ℝ) : ∥(r : ℂ)∥ = ∥r∥ := abs_of_real _ @[simp] lemma norm_rat (r : ℚ) : ∥(r : ℂ)∥ = |(r : ℝ)| := -suffices ∥((r : ℝ) : ℂ)∥ = |r|, by simpa, -by rw [norm_real, real.norm_eq_abs] +by { rw ← of_real_rat_cast, exact norm_real _ } @[simp] lemma norm_nat (n : ℕ) : ∥(n : ℂ)∥ = n := abs_of_nat _ @[simp] lemma norm_int {n : ℤ} : ∥(n : ℂ)∥ = |n| := -suffices ∥((n : ℝ) : ℂ)∥ = |n|, by simpa, -by rw [norm_real, real.norm_eq_abs] +by simp [← rat.cast_coe_int] {single_pass := tt} lemma norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ∥(n : ℂ)∥ = n := -by rw [norm_int, _root_.abs_of_nonneg]; exact int.cast_nonneg.2 hn +by simp [hn] @[continuity] lemma continuous_abs : continuous abs := continuous_norm