Commit 2025-01-29 23:20 d9321524

View on Github →

feat: HasFDerivAt for Fin.cons (#20407) I'm too lazy to add these for Fin.snoc as well, and I suspect people care much less about that. Strictly we need to repeat all these for Matrix.vecCons as well...

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Prod.lean

added theorem HasDerivAt.finCons

added theorem HasDerivAtFilter.finCons

added theorem HasDerivWithinAt.finCons

added theorem HasStrictDerivAt.finCons

added theorem hasDerivAtFilter_finCons'

added theorem hasDerivAtFilter_finCons

added theorem hasDerivAt_finCons'

added theorem hasDerivAt_finCons

added theorem hasDerivWithinAt_finCons'

added theorem hasDerivWithinAt_finCons

added theorem hasStrictDerivAt_finCons'

added theorem hasStrictDerivAt_finCons

Modified Mathlib/Analysis/Calculus/FDeriv/Prod.lean

added theorem Differentiable.finCons

added theorem DifferentiableAt.finCons

added theorem DifferentiableOn.finCons

added theorem DifferentiableWithinAt.finCons

added theorem HasFDerivAt.finCons

added theorem HasFDerivAtFilter.finCons

added theorem HasFDerivWithinAt.finCons

added theorem HasStrictFDerivAt.finCons

added theorem differentiableAt_finCons'

added theorem differentiableAt_finCons

added theorem differentiableOn_finCons'

added theorem differentiableOn_finCons

added theorem differentiableWithinAt_finCons'

added theorem differentiableWithinAt_finCons

added theorem differentiable_finCons'

added theorem differentiable_finCons

added theorem hasFDerivAtFilter_finCons'

added theorem hasFDerivAtFilter_finCons

added theorem hasFDerivAt_finCons'

added theorem hasFDerivAt_finCons

added theorem hasFDerivWithinAt_finCons'

added theorem hasFDerivWithinAt_finCons

added theorem hasStrictFDerivAt_finCons'

added theorem hasStrictFDerivAt_finCons

Modified Mathlib/LinearAlgebra/Pi.lean

added def Fin.consLinearEquiv

modified def LinearMap.vecCons

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added def Fin.consEquivL