Commit 2025-02-26 15:06 2fa582e1

feat: the integral of a constant function is this constant (#22212) Sometimes after a sequence of rewrites one can end up wanting to prove ∫ x, f x ∂μ = c, where f is a complicated expression but which turns out to be constant equal to c. To avoid stating have hf x : f x = c, which can be painful because f is complicated, we introduce the lemma integral_eq_const which directly asks to prove hf.