Skip to content

Define EFTLagrangianExclDeriv for the Higgs field#1459

Draft
nateabr wants to merge 8 commits into
leanprover-community:masterfrom
nateabr:higgs-symmetric
Draft

Define EFTLagrangianExclDeriv for the Higgs field#1459
nateabr wants to merge 8 commits into
leanprover-community:masterfrom
nateabr:higgs-symmetric

feat(Higgs): define normSqTerm and compute its field-content projection

074d4ef
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

2 errors and 1 warning
Lean based style linters
failed Jul 25, 2026 in 39m 30s