therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.32.0

Coe Add Monoid Hom apply eq bosonic plus fermionic

FieldSpecification.WickAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic

Project documentation

The projection of š“•.WickAlgebra to statSubmodule (š“• := š“•) fermionic. -/ def fermionicProj : š“•.WickAlgebra ā†’ā‚—[ā„‚] statSubmodule (š“• := š“•) fermionic where toFun := Quotient.lift fermionicProjFree fermionicProjFree_eq_of_equiv map_add' x y := by obtain āŸØx, hxāŸ© := Ī¹_surjective x obtain āŸØy, hyāŸ© := Ī¹_surjective y subst hx hy rw [ā† map_add, Ī¹_apply, Ī¹_ap...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record