Commit 2023-06-01 13:13 859c9ce6

View on Github →

feat: lemmas about derivatives of affine maps (#4508)

Estimated changes

Modified Mathlib.lean

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

added theorem HasStrictDerivAt.add_const

added theorem HasStrictDerivAt.const_add

Created Mathlib/Analysis/Calculus/Deriv/AffineMap.lean

added theorem AffineMap.hasDerivAt

added theorem AffineMap.hasDerivAtFilter

added theorem AffineMap.hasDerivAt_lineMap

added theorem AffineMap.hasDerivWithinAt

added theorem AffineMap.hasDerivWithinAt_lineMap

added theorem AffineMap.hasStrictDerivAt

added theorem AffineMap.hasStrictDerivAt_lineMap