MIL/C08_Hierarchies/solutions/Solutions_S03_Subobjects.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. structure Submonoid₁ line 8 source

    no axioms what this means

    Statement uses: Monoid

    Also declared: MIL/C08_Hierarchies/S03_Subobjects.lean:8 (same declaration text).

  2. instance (instance at line 17) line 17 source

    Source documentation

    Submonoids in M can be seen as sets in M.

    instance [Monoid M] : SetLike (Submonoid₁ M) M where
…

    Mentions: Submonoid₁

  3. example (example at line 23) line 23 source
  4. example (example at line 25) line 25 source
  5. example (example at line 28) line 28 source
  6. instance SubMonoid₁Monoid line 31 source

    no axioms what this means

    Statement uses: Monoid, Submonoid₁, Subtype, Membership.mem

    Proof uses: Monoid.mk, Semigroup.mk, Mul.mk, Subtype.mk, HMul.hMul, One.mk, OfNat.ofNat, Submonoid₁.one_mem, npowRecAuto

    17 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/S03_Subobjects.lean:31 (same declaration text).

  7. example (example at line 39) line 39 source
  8. class SubmonoidClass₁ line 47 source

    no axioms what this means

    Statement uses: Monoid, SetLike

    Also declared: MIL/C08_Hierarchies/S03_Subobjects.lean:47 (same declaration text).

  9. instance (instance at line 51) line 51 source
  10. structure Subgroup₁ line 56 source

    standard axioms: propext what this means

    Statement uses: Group

  11. instance (instance at line 62) line 62 source

    Source documentation

    Subgroups in M can be seen as sets in M.

    instance [Group G] : SetLike (Subgroup₁ G) G where
…

    Mentions: Subgroup₁

  12. instance (instance at line 66) line 66 source
  13. class SubgroupClass₁ line 71 source

    standard axioms: propext what this means

    Statement uses: Group, SetLike

  14. instance (instance at line 75) line 75 source
  15. instance (instance at line 79) line 79 source
  16. instance (instance at line 84) line 84 source
  17. example (example at line 91) line 91 source
  18. def Submonoid.Setoid line 94 source

    no axioms what this means

    Statement uses: CommMonoid, Submonoid, Setoid

    Proof uses: Setoid.mk, Exists, And, Membership.mem, Eq, HMul.hMul

    10 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/S03_Subobjects.lean:66 (same statement text; different proof or body). Qualify references as Submonoid.Setoid@path.

    Tactic trace: 3 steps

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

  19. instance (instance at line 105) line 105 source
  20. def QuotientMonoid.mk line 108 source

    no axioms what this means

    Statement uses: CommMonoid, Submonoid, HasQuotient.Quotient

    Proof uses: Quotient.mk, Submonoid.Setoid

    5 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/S03_Subobjects.lean:78 (same declaration text).

    Tactic trace: 15 steps

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

  21. instance (instance at line 110) line 110 source