MIL/C09_Groups_and_Rings/S01_Groups.lean

GitHub source file

62 declarations, 13 contain sorry, 0 declared as axioms

1. example (example at line 8) line 8 source
2. example (example at line 10) line 10 source
3. example (example at line 12) line 12 source
4. example (example at line 15) line 15 source
5. example (example at line 18) line 18 source
6. example (example at line 21) line 21 source
7. example (example at line 23) line 23 source
8. example (example at line 26) line 26 source
9. example (example at line 29) line 29 source
10. example (example at line 32) line 32 source
11. example (example at line 35) line 35 source
12. example (example at line 39) line 39 source
13. example (example at line 43) line 43 source
14. example (example at line 48) line 48 source
15. example (example at line 52) line 52 source
16. example (example at line 56) line 56 source
17. example (example at line 70) line 70 source
18. example (example at line 72) line 72 source
19. example (example at line 74) line 74 source
20. example (example at line 77) line 77 source
21. example (example at line 81) line 81 source
22. example (example at line 83) line 83 source
23. def conjugate sorry line 85 source

    depends on sorry what this means

    Statement uses: Group, Subgroup

    Proof uses: Subgroup.mk, Submonoid.mk, Subsemigroup.mk, setOf, Exists, And, Membership.mem, Eq, HMul.hMul, Inv.inv, id, Set, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    16 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:8 (same statement text; different proof or body). Qualify references as conjugate@path.

    Tactic trace: 10 steps

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

24. example (example at line 97) line 97 source
25. example (example at line 100) line 100 source
26. example (example at line 106) line 106 source
27. example (example at line 110) line 110 source
28. example (example at line 119) sorry line 119 source
29. example (example at line 122) sorry line 122 source
30. example (example at line 128) sorry line 128 source

    Source comment

    Remember you can use the `ext` tactic to prove an equality of subgroups.

    example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
        comap (ψ.comp φ) U = comap φ (comap ψ U) := by
    …

31. example (example at line 134) sorry line 134 source

    Source comment

    Pushing a subgroup along one homomorphism and then another is equal to pushing it forward along the composite of the homomorphisms.

    example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
        map (ψ.comp φ) S = map ψ (S.map φ) := by
    …

    Mentions: S

32. example (example at line 143) line 143 source
33. example (example at line 148) line 148 source
34. lemma eq_bot_iff_card sorry line 152 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, Iff, Eq, Bot.bot, Nat, Nat.card, Subtype, Membership.mem, OfNat.ofNat

    Proof uses: Exists, And, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Eq.mpr, id, congr, congrArg, Eq.trans, Subtype.mk, funext, propext, exists_prop_congr, Iff.of_eq, forall_congr, Subtype.mk.injEq and 1 more

    18 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:74 (same statement text; different proof or body). Qualify references as eq_bot_iff_card@path.

    Tactic trace: 3 steps

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

35. lemma inf_bot_of_coprime sorry line 160 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, Nat.Coprime, Nat.card, Subtype, Membership.mem, Eq, Min.min, Bot.bot

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    9 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:85 (same statement text; different proof or body). Qualify references as inf_bot_of_coprime@path.

    Tactic trace: 1 steps

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

36. example (example at line 165) line 165 source
37. inductive S line 172 source

    no axioms what this means

38. def myElement line 176 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: FreeGroup, S

    Proof uses: HMul.hMul, FreeGroup.of, S.a, Inv.inv, S.b

    3 instances, coercions and auxiliary constants left out.

39. def myMorphism line 178 source

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

    Statement uses: MonoidHom, FreeGroup, S, Equiv.Perm, Fin, OfNat.ofNat, Nat

    Proof uses: Equiv, FreeGroup.lift, myMorphism.match_1, Unit, Cycle.formPerm, List.cons, List.nil

    24 instances, coercions and auxiliary constants left out.

40. def myGroup line 184 source

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

    Proof uses: PresentedGroup, Unit, Singleton.singleton, FreeGroup, Set, HPow.hPow, Nat, FreeGroup.of, Unit.unit, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

41. def myMap line 186 source

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

    Statement uses: Unit, Equiv.Perm, Fin, OfNat.ofNat, Nat

    Proof uses: Cycle.formPerm, List.cons, List.nil

    7 instances, coercions and auxiliary constants left out.

42. lemma compat_myMap line 189 source

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

    Statement uses: FreeGroup, Unit, Membership.mem, Set, Singleton.singleton, HPow.hPow, Nat, FreeGroup.of, Unit.unit, OfNat.ofNat, Eq, Equiv.Perm, Fin, MonoidHom, Equiv, FreeGroup.lift, myMap

    Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, map_pow, FreeGroup.lift_apply_of, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

43. def myNewMorphism line 195 source

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

    Statement uses: MonoidHom, myGroup, Equiv.Perm, Fin, OfNat.ofNat, Nat

    Proof uses: PresentedGroup.toGroup, Unit, myMap, Singleton.singleton, FreeGroup, Set, HPow.hPow, FreeGroup.of, Unit.unit, compat_myMap

    15 instances, coercions and auxiliary constants left out.

44. example (example at line 201) line 201 source
45. example (example at line 205) line 205 source
46. example (example at line 211) line 211 source
47. def CayleyIsoMorphism line 214 source

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

    Statement uses: Group, MulEquiv, Subtype, Equiv.Perm, Membership.mem, Subgroup, MonoidHom.range, MulAction.toPermHom

    Proof uses: Equiv.Perm.subgroupOfMulAction

    14 instances, coercions and auxiliary constants left out.

48. example (example at line 217) line 217 source
49. example (example at line 221) line 221 source
50. example (example at line 225) line 225 source
51. lemma conjugate_one sorry line 230 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, Eq, conjugate, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    11 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:95 (same statement text; different proof or body). Qualify references as conjugate_one@path.

    Tactic trace: 3 steps

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

52. instance (instance at line 233) sorry line 233 source
53. example (example at line 244) line 244 source
54. example (example at line 246) line 246 source
55. example (example at line 249) line 249 source
56. example (example at line 253) line 253 source
57. example (example at line 257) line 257 source
58. example (example at line 262) line 262 source
59. lemma aux_card_eq sorry line 275 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, Finite, Eq, Nat, Nat.card, HMul.hMul, Subtype, Membership.mem, HasQuotient.Quotient

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

    11 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:130 (same statement text; different proof or body). Qualify references as aux_card_eq@path.

    Tactic trace: 1 steps

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

60. def iso₁ sorry line 286 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, Subgroup.Normal, MulEquiv, Subtype, Membership.mem, HasQuotient.Quotient

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    21 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:146 (same statement text; different proof or body). Qualify references as iso₁@path.

    Tactic trace: 1 steps

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

61. def iso₂ sorry line 288 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, Subgroup.Normal, MulEquiv, Prod, HasQuotient.Quotient

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    17 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:155 (same statement text; different proof or body). Qualify references as iso₂@path.

    Tactic trace: 1 steps

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

62. def finalIso sorry line 292 source

    depends on sorry what this means

    Statement uses: Group, Subgroup, MulEquiv, Prod, Subtype, Membership.mem

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    19 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean:164 (same statement text; different proof or body). Qualify references as finalIso@path.