MIL/C08_Hierarchies/S03_Subobjects.lean

GitHub source file

15 declarations, 2 contain sorry, 0 declared as axioms

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

    no axioms what this means

    Statement uses: Monoid

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_S03_Subobjects.lean:47 (same declaration text).

  9. instance (instance at line 51) line 51 source
  10. instance (instance at line 56) line 56 source
  11. example (example at line 63) line 63 source
  12. def Submonoid.Setoid sorry line 66 source

    depends on sorry what this means

    Statement uses: CommMonoid, Submonoid, Setoid

    Proof uses: Setoid.mk, Exists, And, Membership.mem, Eq, HMul.hMul, Equivalence.mk, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    12 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 1 steps

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

  13. instance (instance at line 75) line 75 source
  14. def QuotientMonoid.mk line 78 source

    depends on sorry 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/solutions/Solutions_S03_Subobjects.lean:108 (same declaration text).

    Tactic trace: 4 steps

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

  15. instance (instance at line 80) sorry line 80 source