MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean

GitHub source file

13 declarations, 12 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example (example at line 20) line 20 source
  2. example (example at line 38) sorry line 38 source
  3. example (example at line 41) sorry line 41 source
  4. example (example at line 44) sorry line 44 source
  5. example (example at line 47) sorry line 47 source
  6. theorem absorb1 sorry line 50 source

    depends on sorry what this means

    Statement uses: Lattice, Eq, Min.min, Max.max

    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/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean:64 (same statement text; different proof or body). Qualify references as absorb1@path.

    Tactic trace: 1 steps

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

  7. theorem absorb2 sorry line 53 source

    depends on sorry what this means

    Statement uses: Lattice, Eq, Max.max, Min.min

    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/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean:71 (same statement text; different proof or body). Qualify references as absorb2@path.

    Tactic trace: 7 steps

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

  8. example (example at line 72) sorry line 72 source
  9. example (example at line 75) sorry line 75 source
  10. example (example at line 89) sorry line 89 source
  11. example (example at line 92) sorry line 92 source
  12. example (example at line 95) sorry line 95 source
  13. example (example at line 108) sorry line 108 source