Define `EFTLagrangianExclDeriv` for the Higgs field - #1459

Closed

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
e9c86e4

Commits on Jul 23, 2026

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

Commits on Jul 25, 2026