Define `EFTLagrangianExclDeriv` for the Higgs field#1459

Draft

nateabr wants to merge 8 commits into

leanprover-community:masterfrom

nateabr:higgs-symmetric

Commits on Jul 22, 2026

feat(mathematics): add symmetric maps and symmetric algebra monomials

nateabr
and
codex
committed

Commits on Jul 23, 2026

chore(mathematics): update SymmetricMap author header and module docstring
nateabr
committed
feat(mathematics): add SymmetricAlgebra.liftSymmetric and its linear equivalence
nateabr
committed