FormalConjecturesForMathlib/Algebra/Order/Group/Pointwise/Interval.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)
Imported by 2 files
  1. theorem Nat.image_mul_two_Iio_even line 26 source

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

    Statement uses: Nat, Even, Eq, Set, Set.image, HMul.hMul, OfNat.ofNat, Set.Iio, HDiv.hDiv, Inter.inter, Set.ofPred

    Proof uses: Eq.mpr, Exists, id, congrArg, congrFun', funext, Eq.trans, Dvd.dvd, Eq.mp, mul_div_cancel_left₀, of_eq_true, Not, False, True, not_false_eq_true, Set.ext, Iff, Membership.mem, And, LT.lt and 8 more

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. theorem Nat.image_mul_two_Iio line 30 source

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

    Statement uses: Nat, Eq, Set, Set.image, HMul.hMul, OfNat.ofNat, Set.Iio, HDiv.hDiv, HAdd.hAdd, Inter.inter, Set.ofPred, Even

    Proof uses: Eq.mpr, Exists, id, congr, congrArg, Set.image_congr, Membership.mem, mul_comm, congrFun', funext, Eq.trans, Dvd.dvd, Set.ext, Iff, And, LT.lt, HSub.hSub, of_eq_true, LE.le, True and 8 more

    93 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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