DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-05-16 10:05:05 -04:00
parent f0ef95b628
commit 2cda0a017d
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
HepLean/SpaceTime/LorentzGroup.lean
View file

@ -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 _)