FLT/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem AbsoluteValue.inv_pos line 28 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, LT.lt, OfNat.ofNat, Inv.inv

   Proof uses: Eq.mpr, id, Eq, congrArg, IsAbsoluteValue.abv_inv, propext, inv_pos

   52 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

2. theorem AbsoluteValue.ne_zero_of_lt_one line 31 source

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

   Statement uses: Field, LinearOrder, IsStrictOrderedRing, AbsoluteValue, LT.lt, OfNat.ofNat, Ne

   Proof uses: Eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one and 25 more

   65 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

3. theorem AbsoluteValue.isNontrivial_iff_exists_abv_gt_one line 35 source

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

   Statement uses: Field, LinearOrder, IsStrictOrderedRing, AbsoluteValue, Iff, AbsoluteValue.IsNontrivial, Exists, LT.lt, OfNat.ofNat

   Proof uses: Iff.intro, AbsoluteValue.IsNontrivial.exists_abv_gt_one, Exists.intro, And, Ne, Inv.inv, And.intro, Eq.mpr, Not, Eq, id, congrArg, AbsoluteValue.ne_zero_of_lt_one, Eq.trans, congrFun', map_inv₀, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd and 44 more

   88 instances, coercions and auxiliary constants left out.

   Tactic trace: 8 steps

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

4. theorem AbsoluteValue.inv_lt_one_iff line 44 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, Iff, LT.lt, Inv.inv, OfNat.ofNat, Or, Eq

   Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LE.le, map_inv₀, iff_self

   68 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

5. theorem AbsoluteValue.mul_one_div_lt_iff line 47 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, LT.lt, OfNat.ofNat, Iff, HMul.hMul, HDiv.hDiv

   Proof uses: Eq.mpr, id, Eq, congrArg, map_mul, Inv.inv, one_div, map_inv₀, propext, mul_inv_lt_iff₀, one_mul, Iff.rfl

   77 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

6. theorem AbsoluteValue.mul_one_div_pow_lt_iff line 51 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, Nat, LT.lt, OfNat.ofNat, Iff, HMul.hMul, HDiv.hDiv, HPow.hPow

   Proof uses: Eq.rec, Eq, AbsoluteValue.mul_one_div_lt_iff, pow_pos, Eq.symm, map_pow

   68 instances, coercions and auxiliary constants left out.

7. theorem AbsoluteValue.one_lt_of_lt_one line 55 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, LT.lt, OfNat.ofNat

   Proof uses: Or.resolve_left, Eq, Iff.mp, Inv.inv, Or, AbsoluteValue.inv_lt_one_iff, Eq.rec, inv_lt_one_of_one_lt₀, Eq.symm, map_inv₀, AbsoluteValue.ne_zero_of_lt_one

   54 instances, coercions and auxiliary constants left out.

8. theorem AbsoluteValue.one_lt_iff_of_lt_one_iff line 59 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, Iff, LT.lt, OfNat.ofNat

   Proof uses: Iff.intro, AbsoluteValue.one_lt_of_lt_one, Iff.mp, Iff.mpr

   34 instances, coercions and auxiliary constants left out.

9. theorem AbsoluteValue.eq_one_of_lt_one_iff line 63 source

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

   Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, Iff, LT.lt, OfNat.ofNat, Eq

   Proof uses: Or, eq_or_lt_of_le, Iff.mp, Not, LE.le, not_lt, Iff.not, Eq.not_lt, Or.inl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Or.inr, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd and 44 more

   70 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

10. theorem AbsoluteValue.eq_one_iff_of_lt_one_iff line 68 source

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

    Statement uses: Field, LinearOrder, AbsoluteValue, IsStrictOrderedRing, Iff, LT.lt, OfNat.ofNat, Eq

    Proof uses: Iff.intro, AbsoluteValue.eq_one_of_lt_one_iff, Iff.symm

    34 instances, coercions and auxiliary constants left out.

11. theorem AbsoluteValue.pos_of_pos line 74 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Field, LinearOrder, AbsoluteValue, LT.lt, OfNat.ofNat

    Proof uses: Eq.mpr, Ne, id, Eq, congrArg, propext, AbsoluteValue.pos_iff, Eq.mp

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

12. theorem AbsoluteValue.one_add_pow_le line 81 source

    standard axioms: propext what this means

    Statement uses: Ring, PartialOrder, Semiring, AbsoluteValue, IsDomain, Nontrivial, Nat, LE.le, HAdd.hAdd, OfNat.ofNat, HPow.hPow

    Proof uses: le_trans, AbsoluteValue.add_le, Eq.mpr, id, Eq, congrArg, map_one, map_pow, le_refl

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

13. theorem AbsoluteValue.one_sub_pow_le line 87 source

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

    Statement uses: CommRing, PartialOrder, IsOrderedRing, Ring, AbsoluteValue, NoZeroDivisors, IsDomain, Nontrivial, Nat, LE.le, HSub.hSub, OfNat.ofNat, HPow.hPow, HAdd.hAdd

    Proof uses: le_trans, Eq.mpr, id, Eq, congrArg, map_one, map_pow, le_refl, AbsoluteValue.le_add

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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