MIL/C08_Hierarchies/S02_Morphisms.lean

GitHub source file

26 declarations, 1 contain sorry, 0 declared as axioms

1. def isMonoidHom₁ line 7 source

   no axioms what this means

   Statement uses: Monoid

   Proof uses: And, Eq, OfNat.ofNat, HMul.hMul

   6 instances, coercions and auxiliary constants left out.

   Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:7 (same declaration text).

2. structure isMonoidHom₂ line 9 source

   no axioms what this means

   Statement uses: Monoid

   Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:9 (same declaration text).

3. example (example at line 12) line 12 source
4. structure MonoidHom₁ line 14 source

   no axioms what this means

   Statement uses: Monoid

   Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:14 (same declaration text).

5. instance (instance at line 19) line 19 source
6. example (example at line 25) line 25 source
7. structure AddMonoidHom₁ line 28 source

   no axioms what this means

   Statement uses: AddMonoid

   Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:28 (same declaration text).

8. instance (instance at line 33) line 33 source
9. structure RingHom₁ line 39 source

   no axioms what this means

   Statement uses: Ring

   Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:39 (same declaration text).

10. class MonoidHomClass₁ line 43 source

    no axioms what this means

    Statement uses: Monoid

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:43 (same declaration text).

11. def badInst line 49 source

    no axioms what this means

    Statement uses: Monoid, MonoidHomClass₁, CoeFun

    Proof uses: CoeFun.mk, MonoidHomClass₁.toFun

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:49 (same declaration text).

12. class MonoidHomClass₂ line 53 source

    no axioms what this means

    Statement uses: outParam, Monoid

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:53 (same declaration text).

13. instance (instance at line 58) line 58 source
14. instance (instance at line 64) line 64 source
15. instance (instance at line 69) line 69 source
16. lemma map_inv_of_inv line 75 source

    no axioms what this means

    Statement uses: Monoid, MonoidHomClass₂, Eq, HMul.hMul, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, MonoidHomClass₂.map_mul, MonoidHomClass₂.map_one, Eq.refl

    14 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:75 (same declaration text).

    Tactic trace: 1 steps

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

17. example (example at line 79) line 79 source
18. example (example at line 82) line 82 source
19. class MonoidHomClass₃ line 87 source

    no axioms what this means

    Statement uses: outParam, Monoid

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:87 (same declaration text).

20. instance (instance at line 92) line 92 source
21. structure OrderPresHom line 100 source

    no axioms what this means

    Statement uses: LE

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:100 (same declaration text).

22. structure OrderPresMonoidHom line 105 source

    no axioms what this means

    Statement uses: Monoid, LE

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:105 (same declaration text).

23. class OrderPresHomClass line 108 source

    no axioms what this means

    Statement uses: outParam, LE

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean:108 (different declaration text). Qualify references as OrderPresHomClass@path.

24. instance (instance at line 110) line 110 source
25. instance (instance at line 112) line 112 source
26. instance (instance at line 115) sorry line 115 source