MIL/C05_Elementary_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
  1. theorem even_of_even_sqr line 5 source

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

    Statement uses: Nat, Dvd.dvd, OfNat.ofNat, HPow.hPow

    Proof uses: Or, Eq, Eq.mp, HMul.hMul, congrArg, propext, Nat.Prime.dvd_mul, Nat.prime_two, pow_two, Or.inl, Or.inr, Eq.refl

    16 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean:41 (same declaration text).

    Tactic trace: 53 steps

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

  2. example (example at line 9) line 9 source
  3. example (example at line 34) line 34 source
  4. theorem factorization_mul' line 61 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, Finsupp, Nat.factorization, HMul.hMul, HAdd.hAdd

    Proof uses: Eq.mpr, id, congrArg, Nat.factorization_mul, Eq.refl

    21 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean:77 (same declaration text).

    Tactic trace: 2 steps

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

  5. theorem factorization_pow' line 66 source

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

    Statement uses: Nat, Eq, Finsupp, Nat.factorization, HPow.hPow, HMul.hMul

    Proof uses: Eq.mpr, HSMul.hSMul, id, congrArg, Nat.factorization_pow, Eq.refl

    21 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean:82 (same declaration text).

    Tactic trace: 2 steps

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

  6. theorem Nat.Prime.factorization' line 71 source

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

    Statement uses: Nat, Nat.Prime, Eq, Finsupp, Nat.factorization, OfNat.ofNat

    Proof uses: Eq.mpr, Finsupp.single, id, congrArg, Nat.Prime.factorization, of_eq_true, Eq.trans, True, congrFun', Finsupp.single_eq_same, eq_self

    10 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean:87 (same declaration text).

    Tactic trace: 26 steps

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

  7. example (example at line 76) line 76 source
  8. example (example at line 89) line 89 source