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-12-19 15:44:32 +00:00
parent cd63ec0716
commit c739a5eeb8
3 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean
View file

@ -230,7 +230,8 @@ lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
conv_rhs => conv_rhs =>
rhs rhs
rw [extractEquiv] rw [extractEquiv]
simp simp only [List.get_eq_getElem, List.length_cons, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd]
erw [Fin.insertNthEquiv_symm_apply] erw [Fin.insertNthEquiv_symm_apply]
simp only [tail, List.tail_cons, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, simp only [tail, List.tail_cons, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Equiv.piCongrRight, Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm, Equiv.piCongrRight, Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm,

4
HepLean/PerturbationTheory/Wick/OfList.lean
View file

@ -99,13 +99,13 @@ def ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (
sumFiber f (ofList l x) sumFiber f (ofList l x)
lemma ofListLift_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] : lemma ofListLift_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
ofListLift f [] 1 = 1 := by ofListLift f [] 1 = 1 := by
simp only [ofListLift, EmbeddingLike.map_eq_one_iff] simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
rw [ofList_empty] rw [ofList_empty]
exact map_one (sumFiber f) exact map_one (sumFiber f)
lemma ofListLift_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) : lemma ofListLift_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
ofListLift f [] x = x • 1 := by ofListLift f [] x = x • 1 := by
simp only [ofListLift, EmbeddingLike.map_eq_one_iff] simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
rw [ofList_eq_smul_one] rw [ofList_eq_smul_one]
rw [ofList_empty] rw [ofList_empty]

2
HepLean/PerturbationTheory/Wick/SuperCommute.lean
View file

@ -208,7 +208,7 @@ lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c` `[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
and for `n=1` is `b [a, c]`. -/ and for `n=1` is `b [a, c]`. -/
def superCommuteSplit {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ) def superCommuteSplit {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ)
(hn : n < lb.length) : FreeAlgebra ℂ I := (hn : n < lb.length) : FreeAlgebra ℂ I :=
superCommuteCoef q la (List.take n lb) • superCommuteCoef q la (List.take n lb) •
ofList (List.take n lb) 1 * ofList (List.take n lb) 1 *
superCommute q (ofList la xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩)) superCommute q (ofList la xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩))