MIL/C06_Discrete_Mathematics/solutions/Solutions_S02_Counting_Arguments.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def triangle line 7 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/S02_Counting_Arguments.lean:48 (same declaration text).

   Tactic trace: 35 steps

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

2. example (example at line 9) line 9 source
3. def triangle' line 37 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/S02_Counting_Arguments.lean:102 (same declaration text).

   Tactic trace: 33 steps

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

4. example (example at line 39) line 39 source
5. example (example at line 52) line 52 source