From 2cda0a017d5cdf74595f8cda7b914ceb8f9aac02 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 10:05:05 -0400 Subject: [PATCH] refactor: Lint --- HepLean/SpaceTime/LorentzGroup.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/HepLean/SpaceTime/LorentzGroup.lean b/HepLean/SpaceTime/LorentzGroup.lean index 1b858e9..372eaf5 100644 --- a/HepLean/SpaceTime/LorentzGroup.lean +++ b/HepLean/SpaceTime/LorentzGroup.lean @@ -199,9 +199,9 @@ lemma fst_col_normalized (Λ : lorentzGroup) : simp only [Fin.isValue, mul_apply, transpose_apply, Fin.sum_univ_four, ne_eq, zero_ne_one, not_false_eq_true, η_off_diagonal, zero_mul, add_zero, Fin.reduceEq, one_ne_zero, mul_zero, zero_add, one_apply_eq] at h00 - simp only [η, Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const, - one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two, Nat.succ_eq_add_one, - Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00 + simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, + vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two, + Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00 rw [← h00] ring @@ -245,7 +245,6 @@ lemma norm_row_leq_abs_zero_zero (Λ : lorentzGroup) : ‖fstRowToEuclid Λ‖ simp only [le_add_iff_nonneg_left, zero_le_one] - lemma zero_zero_sq_ge_one (Λ : lorentzGroup) : 1 ≤ (Λ.1 0 0) ^ 2 := by rw [zero_zero_sq_col Λ] refine le_add_of_le_of_nonneg ?_ (sq_nonneg _)