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

refactor: Simplify normal order

Browse source
This commit is contained in:
jstoobysmith 2025-01-29 15:33:40 +00:00
parent 9107115620
commit a329661c24
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
View file

@ -221,15 +221,13 @@ lemma ι_normalOrder_eq_of_equiv (a b : 𝓕.CrAnAlgebra) (h : a ≈ b) :
noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
toFun := Quotient.lift (ι.toLinearMap ∘ₗ CrAnAlgebra.normalOrder) ι_normalOrder_eq_of_equiv
map_add' x y := by
obtain ⟨x, hx⟩ := ι_surjective x
obtain ⟨y, hy⟩ := ι_surjective y
subst hx hy
obtain ⟨x, rfl⟩ := ι_surjective x
obtain ⟨y, rfl⟩ := ι_surjective y
rw [← map_add, ι_apply, ι_apply, ι_apply]
rw [Quotient.lift_mk, Quotient.lift_mk, Quotient.lift_mk]
simp
map_smul' c y := by
obtain ⟨y, hy⟩ := ι_surjective y
subst hy
obtain ⟨y, rfl⟩ := ι_surjective y
rw [← map_smul, ι_apply, ι_apply]
simp