Generalize integration_by_parts#1674

Open

IshiguroYoshihiro wants to merge 30 commits intomath-comp:masterfrom

IshiguroYoshihiro:integration_by_partsy_20250704

Commits on Feb 19, 2026

rename and boolify some predicates for open intervals
t6s
committed
address review comments
t6s
committed
revert experimental Arguments declaration
t6s
committed
integration_by_party

IshiguroYoshihiro
authored and
t6s
committed
upd and rebase

affeldt-aist
authored and
t6s
committed
lint

affeldt-aist
authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/ftc.v

authored and
t6s
committed
Update theories/realfun.v

authored and
t6s
committed
fix

IshiguroYoshihiro
authored and
t6s
committed
minor fix

IshiguroYoshihiro
authored and
t6s
committed
wip cleaning Let

IshiguroYoshihiro
authored and
t6s
committed
prove admit

affeldt-aist
authored and
t6s
committed
rename: derivable_oy_continuous_bndN -> derivable_oy_RcontinuousN
t6s
committed