Update sam. 09 sept. 2023 20:30:18 EDT

Changes

14 changed files (+19/-5)

• MIL.lean
  • @@ -31,3 +31,4 @@ import MIL.C09_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces
    import MIL.C10_Integration_and_Measure_Theory.S01_Elementary_Integration import MIL.C10_Integration_and_Measure_Theory.S02_Measure_Theory import MIL.C10_Integration_and_Measure_Theory.S03_Integration + import MIL.Common
• MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  • @@ -102,7 +102,7 @@ example (a b : ℝ) : a - b = a + -b := by
    namespace MyRing variable {R : Type*} [Ring R] - theorem self_sub (a : R) : a - a = 0 := + theorem self_sub (a : R) : a - a = 0 := by sorry theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
• MIL/C03_Logic/S02_The_Existential_Quantifier.lean
  • @@ -1,6 +1,8 @@
    import MIL.Common import Mathlib.Data.Real.Basic + set_option autoImplicit true + namespace C03S02 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
• MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean
  • @@ -1,6 +1,8 @@
    import MIL.Common import Mathlib.Data.Real.Basic + set_option autoImplicit true + namespace C03S02 def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
• MIL/C07_Hierarchies/S01_Basics.lean
  • @@ -2,6 +2,8 @@ import MIL.Common
    import Mathlib.Algebra.BigOperators.Ring import Mathlib.Data.Real.Basic + set_option autoImplicit true + class One₁ (α : Type) where /-- The element one -/
• MIL/C07_Hierarchies/S02_Morphisms.lean
  • @@ -1,6 +1,8 @@
    import MIL.Common import Mathlib.Topology.Instances.Real + set_option autoImplicit true + def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop := f 1 = 1 ∧ ∀ g g', f (g * g') = f g * f g'
• MIL/C07_Hierarchies/S03_Subobjects.lean
  • @@ -1,6 +1,7 @@
    import MIL.Common import Mathlib.GroupTheory.QuotientGroup + set_option autoImplicit true @[ext]
• MIL/C07_Hierarchies/solutions/Solutions_S01_Basics.lean
  • @@ -2,6 +2,8 @@ import MIL.Common
    import Mathlib.Algebra.BigOperators.Ring import Mathlib.Data.Real.Basic + set_option autoImplicit true + class One₁ (α : Type) where /-- The element one -/
• MIL/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean
  • @@ -1,6 +1,8 @@
    import MIL.Common import Mathlib.Topology.Instances.Real + set_option autoImplicit true + def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop := f 1 = 1 ∧ ∀ g g', f (g * g') = f g * f g'
• MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean
  • @@ -1,6 +1,7 @@
    import MIL.Common import Mathlib.GroupTheory.QuotientGroup + set_option autoImplicit true @[ext]
• README.md
  • @@ -13,7 +13,7 @@ Alternatively, you can use Gitpod to run Lean and VS Code in the cloud.
    This version of *Mathematics in Lean* is designed for [Lean 4](https://leanprover.github.io/) and [Mathlib](https://github.com/leanprover-community/mathlib4). - For the Lean 3 version, see [github.com/leanprover-community/mathematics_in_lean3](github.com/leanprover-community/mathematics_in_lean3). + For the Lean 3 version, see [https://github.com/leanprover-community/mathematics_in_lean3](https://github.com/leanprover-community/mathematics_in_lean3). ## To use this repository on your computer
• html/C02_Basics.html
  • @@ -635,7 +635,7 @@ but in some contexts, when dealing with the real numbers,
    you can use the two sides of the equation interchangeably. For example, you now have enough information to prove the theorem <code class="docutils literal notranslate"><span class="pre">self_sub</span></code> from the last section:</p> - <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">self_sub</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> + <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">self_sub</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span> </pre></div> </div>
• lakefile.lean
  • @@ -3,8 +3,7 @@ open Lake DSL
    def moreServerArgs := #[ "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b` - -- this is set in mathlib, but the exercises are nicer to read without it - -- "-DautoImplicit=false", + "-DautoImplicit=false", "-DrelaxedAutoImplicit=false" ]
• mathematics_in_lean.pdf