Solutions_S01_Groups.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)

def conjugate line 8 source
standard axioms: Classical.choice, Quot.sound, propext 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
15 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:85 (same statement text; different proof or body). Qualify references as conjugate@path.
Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
example (example at line 32) line 32 source
example (example at line 37) line 37 source
example (example at line 46) line 46 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
…
```
example (example at line 55) line 55 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
lemma eq_bot_iff_card line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Iff, Eq, Bot.bot, Nat, Nat.card, Subtype, Membership.mem, OfNat.ofNat
Proof uses: Exists, And, Iff.intro, Exists.intro, And.intro, Subgroup.one_mem, Trans.trans, Eq.symm, 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
21 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:152 (same statement text; different proof or body). Qualify references as eq_bot_iff_card@path.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma inf_bot_of_coprime line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Nat.Coprime, Nat.card, Subtype, Membership.mem, Eq, Min.min, Bot.bot
Proof uses: Dvd.dvd, Nat, Subgroup.card_dvd_of_le, inf_le_left, inf_le_right, Iff.mpr, OfNat.ofNat, eq_bot_iff_card, Nat.eq_one_of_dvd_coprimes
14 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:160 (same statement text; different proof or body). Qualify references as inf_bot_of_coprime@path.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma conjugate_one line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, conjugate, OfNat.ofNat
Proof uses: Subgroup.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congrFun', congrArg, Submonoid, Submonoid.mk, Subsemigroup.mk, Set, setOf, Exists, And, HMul.hMul, Inv.inv, funext, congr, one_mul and 10 more
33 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:230 (same statement text; different proof or body). Qualify references as conjugate_one@path.
Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
instance (instance at line 99) line 99 source
lemma aux_card_eq line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Finite, Eq, Nat, Nat.card, HMul.hMul, Subtype, Membership.mem, HasQuotient.Quotient
Proof uses: Trans.trans, Eq.mpr, Subgroup.index, id, congrArg, Eq.symm, Subgroup.index_eq_card, Subgroup.index_mul_card, Eq.refl, mul_comm, Nat.eq_of_mul_eq_mul_right, Nat.card_pos
19 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:275 (same statement text; different proof or body). Qualify references as aux_card_eq@path.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def iso₁ line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.Normal, Fintype, Disjoint, Eq, Nat, Nat.card, HMul.hMul, Subtype, Membership.mem, MulEquiv, HasQuotient.Quotient
Proof uses: MulEquiv.ofBijective, MonoidHom, MonoidHom.restrict, QuotientGroup.mk'
40 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:286 (same statement text; different proof or body). Qualify references as iso₁@path.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def iso₂ line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.Normal, Fintype, Disjoint, Eq, Nat, Nat.card, HMul.hMul, Subtype, Membership.mem, MulEquiv, Prod, HasQuotient.Quotient
Proof uses: MulEquiv.ofBijective, MonoidHom, MonoidHom.prod, QuotientGroup.mk'
39 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:288 (same statement text; different proof or body). Qualify references as iso₂@path.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def finalIso line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.Normal, Fintype, Disjoint, Eq, Nat, Nat.card, HMul.hMul, Subtype, Membership.mem, MulEquiv, Prod
Proof uses: MulEquiv.trans, HasQuotient.Quotient, iso₂, MulEquiv.symm, MulEquiv.prodCongr, iso₁
39 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C09_Groups_and_Rings/S01_Groups.lean:292 (same statement text; different proof or body). Qualify references as finalIso@path.