MIL/C12_Differential_Calculus/S01_Elementary_Differential_Calculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)
Imported by 1 file
  1. example (example at line 15) line 15 source

    Source documentation

    The sin function has derivative 1 at 0.

    example : HasDerivAt sin 1 0 := by simpa using hasDerivAt_sin 0
  2. example (example at line 17) line 17 source
  3. example (example at line 20) line 20 source
  4. example (example at line 23) line 23 source
  5. example (example at line 26) line 26 source
  6. example (example at line 30) line 30 source
  7. example (example at line 36) line 36 source
  8. example (example at line 40) line 40 source
  9. example (example at line 44) line 44 source
  10. example (example at line 46) line 46 source