MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean

GitHub source file

19 declarations, 4 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. example (example at line 7) line 7 source
  2. example (example at line 10) line 10 source
  3. example (example at line 14) line 14 source
  4. example (example at line 16) line 16 source
  5. example (example at line 20) line 20 source
  6. example (example at line 25) line 25 source
  7. example (example at line 28) line 28 source
  8. example (example at line 31) line 31 source

    Source comment

    commonly used
    example : Nat.Prime 2 :=
…
  9. example (example at line 34) line 34 source
  10. theorem even_of_even_sqr line 41 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/solutions/Solutions_S01_Irrational_Roots.lean:5 (same declaration text).

    Tactic trace: 19 steps

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

  11. example (example at line 45) line 45 source
  12. example (example at line 48) line 48 source
  13. example (example at line 52) sorry line 52 source
  14. example (example at line 70) sorry line 70 source
  15. theorem factorization_mul' line 77 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/solutions/Solutions_S01_Irrational_Roots.lean:61 (same declaration text).

    Tactic trace: 2 steps

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

  16. theorem factorization_pow' line 82 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/solutions/Solutions_S01_Irrational_Roots.lean:66 (same declaration text).

    Tactic trace: 2 steps

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

  17. theorem Nat.Prime.factorization' line 87 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/solutions/Solutions_S01_Irrational_Roots.lean:71 (same declaration text).

    Tactic trace: 25 steps

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

  18. example (example at line 92) sorry line 92 source
  19. example (example at line 104) sorry line 104 source