MIL/C02_Basics/S01_Calculating.lean

GitHub source file

22 declarations, 9 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example (example at line 4) line 4 source

    Source comment

    An example.
    example (a b c : ℝ) : a * b * c = b * (a * c) := by
…
  2. example (example at line 9) sorry line 9 source

    Source comment

    Try these.
    example (a b c : ℝ) : c * b * a = b * (a * c) := by
…
  3. example (example at line 12) sorry line 12 source
  4. example (example at line 16) line 16 source

    Source comment

    An example.
    example (a b c : ℝ) : a * b * c = b * c * a := by
…
  5. example (example at line 22) sorry line 22 source

    Source comment

    Try doing the first of these without providing any arguments at all, and the second with only one argument.
    example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
…
  6. example (example at line 25) sorry line 25 source
  7. example (example at line 29) line 29 source

    Source comment

    Using facts from the local context.
    example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
…

    Mentions: f

  8. example (example at line 35) sorry line 35 source
  9. example (example at line 38) sorry line 38 source
  10. example (example at line 41) line 41 source
  11. example (example at line 48) line 48 source
  12. example (example at line 70) line 70 source
  13. example (example at line 75) line 75 source
  14. example (example at line 84) sorry line 84 source
  15. example (example at line 99) sorry line 99 source
  16. example (example at line 102) sorry line 102 source
  17. example (example at line 119) line 119 source
  18. example (example at line 126) line 126 source
  19. example (example at line 129) line 129 source
  20. example (example at line 132) line 132 source
  21. example (example at line 135) line 135 source
  22. example (example at line 141) line 141 source