FormalConjecturesForMathlib/Algebra/Powerfree.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def Powerfree line 28 source

   no axioms what this means

   Statement uses: Monoid, Nat

   Proof uses: Dvd.dvd, HPow.hPow, IsUnit

   5 instances, coercions and auxiliary constants left out.

2. theorem Powerfree.of_le line 31 source

   standard axioms: propext what this means

   Statement uses: Monoid, Nat, LE.le, Powerfree

   Proof uses: Dvd.dvd, HPow.hPow, dvd_of_mul_right_dvd, HSub.hSub, Eq.rec, Eq, HMul.hMul, Eq.symm, pow_mul_pow_sub

   13 instances, coercions and auxiliary constants left out.

3. theorem Powerfree.of_dvd line 34 source

   no axioms what this means

   Statement uses: Nat, Monoid, Dvd.dvd, Powerfree

   Proof uses: HPow.hPow, Dvd.dvd.trans

   7 instances, coercions and auxiliary constants left out.

4. theorem powerfree_congr line 37 source

   no axioms what this means

   Statement uses: Nat, Monoid, Associated, Iff, Powerfree

   Proof uses: Iff.intro, Powerfree.of_dvd, Associated.dvd', Associated.dvd

5. theorem powerfree_neg line 41 source

   standard axioms: propext what this means

   Statement uses: Nat, Monoid, HasDistribNeg, Iff, Powerfree, Neg.neg

   Proof uses: powerfree_congr, Associated.neg_left, Associated.refl

   10 instances, coercions and auxiliary constants left out.

6. theorem powerfree_two line 45 source

   no axioms what this means

   Statement uses: Monoid, Iff, Powerfree, OfNat.ofNat, Nat, Squarefree

   Proof uses: Iff.intro, Dvd.dvd, HMul.hMul, Eq.rec, Eq, HPow.hPow, Eq.symm, sq

   11 instances, coercions and auxiliary constants left out.

7. theorem IsUnit.powerfree line 54 source

   standard axioms: propext what this means

   Statement uses: Nat, CommMonoid, IsUnit, Ne, OfNat.ofNat, Powerfree

   Proof uses: Dvd.dvd, HPow.hPow, Iff.mp, isUnit_pow_iff, isUnit_of_dvd_unit

   9 instances, coercions and auxiliary constants left out.

8. theorem powerfree_one line 58 source

   standard axioms: propext what this means

   Statement uses: Nat, CommMonoid, Ne, OfNat.ofNat, Powerfree

   Proof uses: IsUnit.powerfree, isUnit_one

   12 instances, coercions and auxiliary constants left out.

9. theorem Irreducible.powerfree line 61 source

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

   Statement uses: Nat, CommMonoid, Irreducible, LE.le, OfNat.ofNat, Powerfree

   Proof uses: Dvd.dvd, HPow.hPow, Eq, HMul.hMul, IsUnit, Nat.recAux, HAdd.hAdd, Or, Irreducible.isUnit_or_isUnit, Eq.mp, congrArg, mul_assoc, pow_succ, Iff.mp, isUnit_pow_iff, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Int, LT.lt, Neg.neg and 50 more

   81 instances, coercions and auxiliary constants left out.

   Tactic trace: 10 steps

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

10. theorem not_powerfree_zero line 75 source

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

    Statement uses: MonoidWithZero, Nontrivial, Nat, Not, Powerfree, OfNat.ofNat

    Proof uses: Eq.mpr, Dvd.dvd, HPow.hPow, IsUnit, id, Eq, congrArg, Powerfree.eq_1, Exists, propext, Classical.not_forall, Exists.intro, of_eq_true, Eq.trans, False, True, implies_congr, not_true_eq_false, not_false_eq_true

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

11. theorem Prime.powerfree line 80 source

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

    Statement uses: Nat, CommMonoidWithZero, IsCancelMulZero, Prime, LE.le, OfNat.ofNat, Powerfree

    Proof uses: Irreducible.powerfree, Prime.irreducible

    16 instances, coercions and auxiliary constants left out.