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-20 14:07:20 +00:00
parent d28b673057
commit b454a7e23c
2 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
HepLean/PerturbationTheory/Wick/Contractions.lean
View file

@ -152,21 +152,21 @@ lemma toCenterTerm_none (f : 𝓕 → Type) [∀ i, Fintype (f i)]
lemma toCenterTerm_center (f : 𝓕 → Type) [∀ i, Fintype (f i)]
(q : 𝓕 → FieldStatistic)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
{r : List 𝓕} → (c : Contractions r) → (S : Splitting f le1) →
(c.toCenterTerm f q le1 F S) ∈ Subalgebra.center ℂ A
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F] :
{r : List 𝓕} → (c : Contractions r) → (S : Splitting f le) →
(c.toCenterTerm f q le F S) ∈ Subalgebra.center ℂ A
| [], ⟨[], .nil⟩, _ => by
dsimp [toCenterTerm]
exact Subalgebra.one_mem (Subalgebra.center ℂ A)
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => by
dsimp [toCenterTerm]
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
exact toCenterTerm_center f q le F ⟨aux', c⟩ S
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => by
dsimp [toCenterTerm]
refine Subalgebra.mul_mem (Subalgebra.center ℂ A) ?hx ?hy
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
exact toCenterTerm_center f q le F ⟨aux', c⟩ S
apply Subalgebra.smul_mem
rw [ofListLift_expand]
rw [map_sum, map_sum]
@ -175,7 +175,7 @@ lemma toCenterTerm_center (f : 𝓕 → Type) [∀ i, Fintype (f i)]
simp only [CreateAnnihilateSect.toList]
rw [ofList_singleton]
exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1)
(le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
(le := le) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
end Contractions

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

@ -132,7 +132,8 @@ def extractEquiv (n : Fin l.length) : CreateAnnihilateSect f l ≃
match l with
| [] => exact Fin.elim0 n
| l0 :: l =>
let e1 : CreateAnnihilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
let e1 : CreateAnnihilateSect f ((l0 :: l).eraseIdx n) ≃
Π i, f ((l0 :: l).get (n.succAbove i)) :=
Equiv.piCongr (Fin.castOrderIso (by rw [eraseIdx_cons_length])).toEquiv
fun x => Equiv.cast (congrArg f (by
rw [HepLean.List.eraseIdx_get]