FormalConjecturesForMathlib/Data/Nat/Factorization/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem Nat.prod_primeFactors_factorization_apply line 24 source

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

    Statement uses: Nat, Nat.Prime, Not, Dvd.dvd, Eq, OfNat.ofNat, Finsupp, Nat.factorization, Finset.prod, Nat.primeFactors, HPow.hPow

    Proof uses: Eq.mpr, Finset.sum, id, congrArg, Nat.factorization_prod, Membership.mem, Finset, False.elim, False, Eq.mp, And, Eq.trans, congr, congrFun', and_false, HSMul.hSMul, Finsupp.single, Finset.sum_congr, rfl, Nat.factorization_pow and 25 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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