MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean

GitHub source file

22 declarations, 3 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. example (example at line 9) line 9 source
  2. example (example at line 10) line 10 source
  3. example (example at line 12) line 12 source
  4. example (example at line 14) line 14 source
  5. example (example at line 15) line 15 source
  6. example (example at line 17) line 17 source
  7. example (example at line 19) line 19 source
  8. example (example at line 26) line 26 source
  9. example (example at line 28) line 28 source
  10. example (example at line 30) line 30 source
  11. example (example at line 34) line 34 source
  12. example (example at line 36) line 36 source
  13. example (example at line 42) line 42 source
  14. def triangle line 48 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Finset, Prod

    Proof uses: Finset.filter, LT.lt, Prod.fst, Prod.snd, SProd.sprod, Finset.range, HAdd.hAdd, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S02_Counting_Arguments.lean:7 (same declaration text).

    Tactic trace: 55 steps

    Open to load the checked before-and-after goal states.

  15. example (example at line 50) line 50 source
  16. example (example at line 70) line 70 source
  17. example (example at line 89) sorry line 89 source
  18. def triangle' line 102 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Finset, Prod

    Proof uses: Finset.filter, LE.le, Prod.fst, Prod.snd, SProd.sprod, Finset.range

    3 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S02_Counting_Arguments.lean:37 (same declaration text).

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  19. example (example at line 104) sorry line 104 source
  20. theorem doubleCounting line 110 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Membership.mem, LE.le, Nat, OfNat.ofNat, Finset.card, Finset.filter, HMul.hMul

    Proof uses: Trans.trans, Finset.sum, Eq, ite, of_eq_true, Eq.trans, True, congr, congrArg, mul_comm, Finset.sum_const, eq_self, Finset.sum_le_sum, Finset.sum_congr, Eq.refl, Finset.sum_boole, Finset.sum_comm, congrFun', HSMul.hSMul, mul_one

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

    Open to load the checked before-and-after goal states.

  21. example (example at line 124) line 124 source
  22. example (example at line 126) sorry line 126 source