MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem MyRing.add_neg_cancel_right line 8 source

   standard axioms: propext what this means

   Statement uses: Ring, Eq, HAdd.hAdd, Neg.neg

   Proof uses: Eq.mpr, id, congrArg, add_assoc, OfNat.ofNat, add_neg_cancel, add_zero, Eq.refl

   34 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:55 (same statement text; different proof or body). Qualify references as MyRing.add_neg_cancel_right@path.

   Tactic trace: 1 steps

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

2. theorem MyRing.add_left_cancel line 11 source

   no axioms what this means

   Statement uses: Ring, Eq, HAdd.hAdd

   Proof uses: Eq.mpr, Neg.neg, id, congrArg, Eq.symm, neg_add_cancel_left, Eq.refl

   16 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:58 (same statement text; different proof or body). Qualify references as MyRing.add_left_cancel@path.

   Tactic trace: 1 steps

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

3. theorem MyRing.add_right_cancel line 14 source

   standard axioms: propext what this means

   Statement uses: Ring, Eq, HAdd.hAdd

   Proof uses: Eq.mpr, Neg.neg, id, congrArg, Eq.symm, MyRing.add_neg_cancel_right, Eq.refl

   14 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:61 (same statement text; different proof or body). Qualify references as MyRing.add_right_cancel@path.

   Tactic trace: 1 steps

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

4. theorem MyRing.zero_mul line 17 source

   no axioms what this means

   Statement uses: Ring, Eq, HMul.hMul, OfNat.ofNat

   Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, add_mul, add_zero, Eq.refl, MyRing.add_left_cancel

   24 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:69 (same statement text; different proof or body). Qualify references as MyRing.zero_mul@path.

   Tactic trace: 3 steps

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

5. theorem MyRing.neg_eq_of_add_eq_zero line 21 source

   standard axioms: propext what this means

   Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat, Neg.neg

   Proof uses: Eq.mpr, id, congrArg, Eq.symm, neg_add_cancel_left, add_zero, Eq.refl

   37 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:72 (same statement text; different proof or body). Qualify references as MyRing.neg_eq_of_add_eq_zero@path.

   Tactic trace: 1 steps

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

6. theorem MyRing.eq_neg_of_add_eq_zero line 24 source

   standard axioms: propext what this means

   Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat, Neg.neg

   Proof uses: Eq.symm, MyRing.neg_eq_of_add_eq_zero, Eq.mpr, id, congrArg, add_comm, Eq.refl

   33 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:75 (same statement text; different proof or body). Qualify references as MyRing.eq_neg_of_add_eq_zero@path.

   Tactic trace: 3 steps

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

7. theorem MyRing.neg_zero line 29 source

   standard axioms: propext what this means

   Statement uses: Ring, Eq, Neg.neg, OfNat.ofNat

   Proof uses: MyRing.neg_eq_of_add_eq_zero, Eq.mpr, HAdd.hAdd, id, congrArg, add_zero, Eq.refl

   24 instances, coercions and auxiliary constants left out.

   Also declared: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:78 (same declaration text).

   Tactic trace: 2 steps

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

8. theorem MyRing.neg_neg line 33 source

   standard axioms: propext what this means

   Statement uses: Ring, Eq, Neg.neg

   Proof uses: MyRing.neg_eq_of_add_eq_zero, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, congrArg, neg_add_cancel, Eq.refl

   28 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:82 (same statement text; different proof or body). Qualify references as MyRing.neg_neg@path.

   Tactic trace: 2 steps

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

9. theorem MyRing.self_sub line 42 source

   no axioms what this means

   Statement uses: Ring, Eq, HSub.hSub, OfNat.ofNat

   Proof uses: Eq.mpr, HAdd.hAdd, Neg.neg, id, congrArg, sub_eq_add_neg, add_neg_cancel, Eq.refl

   25 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:105 (same statement text; different proof or body). Qualify references as MyRing.self_sub@path.

   Tactic trace: 1 steps

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

10. theorem MyRing.one_add_one_eq_two line 45 source

    standard axioms: propext what this means

    Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat, Nat

    Proof uses: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.instAtLeastTwo

    29 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:108 (same declaration text).

    Tactic trace: 1 steps

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

11. theorem MyRing.two_mul line 48 source

    standard axioms: propext what this means

    Statement uses: Ring, Eq, HMul.hMul, OfNat.ofNat, Nat, HAdd.hAdd

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, MyRing.one_add_one_eq_two, add_mul, one_mul, Eq.refl

    34 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:111 (same statement text; different proof or body). Qualify references as MyRing.two_mul@path.

    Tactic trace: 1 steps

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

12. theorem MyGroup.mul_inv_cancel line 58 source

    standard axioms: propext what this means

    Statement uses: Group, Eq, HMul.hMul, Inv.inv, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, mul_assoc, Eq.symm, inv_mul_cancel, one_mul, Eq.refl

    28 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:134 (same statement text; different proof or body). Qualify references as MyGroup.mul_inv_cancel@path.

    Tactic trace: 3 steps

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

13. theorem MyGroup.mul_one line 63 source

    standard axioms: propext what this means

    Statement uses: Group, Eq, HMul.hMul, OfNat.ofNat

    Proof uses: Eq.mpr, Inv.inv, id, congrArg, Eq.symm, inv_mul_cancel, mul_assoc, MyGroup.mul_inv_cancel, one_mul, Eq.refl

    27 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:137 (same statement text; different proof or body). Qualify references as MyGroup.mul_one@path.

    Tactic trace: 1 steps

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

14. theorem MyGroup.mul_inv_rev line 66 source

    standard axioms: propext what this means

    Statement uses: Group, Eq, Inv.inv, HMul.hMul

    Proof uses: Eq.mpr, OfNat.ofNat, id, congrArg, Eq.symm, one_mul, inv_mul_cancel, mul_assoc, MyGroup.mul_inv_cancel, MyGroup.mul_one, Eq.refl

    26 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean:140 (same statement text; different proof or body). Qualify references as MyGroup.mul_inv_rev@path.

    Tactic trace: 1 steps

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