Skip to content

feat: multiplication by a regular function in D^n as a CLM (bilin version)#41485

Open
luigi-massacci wants to merge 26 commits into
leanprover-community:masterfrom
luigi-massacci:LM_mul_distrib_II
Open

feat: multiplication by a regular function in D^n as a CLM (bilin version)#41485
luigi-massacci wants to merge 26 commits into
leanprover-community:masterfrom
luigi-massacci:LM_mul_distrib_II

Commits

Commits on Jun 20, 2026

Commits on Jun 24, 2026

Commits on Jul 3, 2026