bump to nightly-2023-06-06-13

mathlib commit leanprover-community/mathlib@a3209dd

Mathbin/LinearAlgebra/QuadraticForm/Isometry.lean

@@ -35,19 +35,23 @@ variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMon
 
 variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃]
 
+#print QuadraticForm.Isometry /-
 /-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
 is a linear equivalence between `M₁` and `M₂` that commutes with the quadratic forms. -/
 @[nolint has_nonempty_instance]
 structure Isometry (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) extends M₁ ≃ₗ[R] M₂ where
   map_app' : ∀ m, Q₂ (to_fun m) = Q₁ m
 #align quadratic_form.isometry QuadraticForm.Isometry
+-/
 
+#print QuadraticForm.Equivalent /-
 /-- Two quadratic forms over a ring `R` are equivalent
 if there exists an isometry between them:
 a linear equivalence that transforms one quadratic form into the other. -/
 def Equivalent (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :=
   Nonempty (Q₁.Isometry Q₂)
 #align quadratic_form.equivalent QuadraticForm.Equivalent
+-/
 
 namespace Isometry
 
@@ -65,34 +69,40 @@ instance : CoeFun (Q₁.Isometry Q₂) fun _ => M₁ → M₂ :=
   ⟨fun f => ⇑(f : M₁ ≃ₗ[R] M₂)⟩
 
 @[simp]
-theorem coe_to_linearEquiv (f : Q₁.Isometry Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f :=
+theorem coe_toLinearEquiv (f : Q₁.Isometry Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f :=
   rfl
-#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.Isometry.coe_to_linearEquiv
+#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.Isometry.coe_toLinearEquiv
 
 @[simp]
 theorem map_app (f : Q₁.Isometry Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
   f.map_app' m
 #align quadratic_form.isometry.map_app QuadraticForm.Isometry.map_app
 
+#print QuadraticForm.Isometry.refl /-
 /-- The identity isometry from a quadratic form to itself. -/
 @[refl]
 def refl (Q : QuadraticForm R M) : Q.Isometry Q :=
   { LinearEquiv.refl R M with map_app' := fun m => rfl }
 #align quadratic_form.isometry.refl QuadraticForm.Isometry.refl
+-/
 
+#print QuadraticForm.Isometry.symm /-
 /-- The inverse isometry of an isometry between two quadratic forms. -/
 @[symm]
 def symm (f : Q₁.Isometry Q₂) : Q₂.Isometry Q₁ :=
   { (f : M₁ ≃ₗ[R] M₂).symm with
     map_app' := by intro m; rw [← f.map_app]; congr; exact f.to_linear_equiv.apply_symm_apply m }
 #align quadratic_form.isometry.symm QuadraticForm.Isometry.symm
+-/
 
+#print QuadraticForm.Isometry.trans /-
 /-- The composition of two isometries between quadratic forms. -/
 @[trans]
 def trans (f : Q₁.Isometry Q₂) (g : Q₂.Isometry Q₃) : Q₁.Isometry Q₃ :=
   { (f : M₁ ≃ₗ[R] M₂).trans (g : M₂ ≃ₗ[R] M₃) with
     map_app' := by intro m; rw [← f.map_app, ← g.map_app]; rfl }
 #align quadratic_form.isometry.trans QuadraticForm.Isometry.trans
+-/
 
 end Isometry
 
@@ -119,6 +129,7 @@ end Equivalent
 
 variable [Fintype ι] {v : Basis ι R M}
 
+#print QuadraticForm.isometryOfCompLinearEquiv /-
 /-- A quadratic form composed with a `linear_equiv` is isometric to itself. -/
 def isometryOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) :
     Q.Isometry (Q.comp (f : M₁ →ₗ[R] M)) :=
@@ -128,12 +139,15 @@ def isometryOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) :
       simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
         LinearEquiv.apply_symm_apply, f.apply_symm_apply] }
 #align quadratic_form.isometry_of_comp_linear_equiv QuadraticForm.isometryOfCompLinearEquiv
+-/
 
+#print QuadraticForm.isometryBasisRepr /-
 /-- A quadratic form is isometric to its bases representations. -/
 noncomputable def isometryBasisRepr (Q : QuadraticForm R M) (v : Basis ι R M) :
     Isometry Q (Q.basis_repr v) :=
   isometryOfCompLinearEquiv Q v.equivFun.symm
 #align quadratic_form.isometry_basis_repr QuadraticForm.isometryBasisRepr
+-/
 
 variable [Field K] [Invertible (2 : K)] [AddCommGroup V] [Module K V]
 

Mathbin/RingTheory/DedekindDomain/Factorization.lean

@@ -37,11 +37,13 @@ open Set Function UniqueFactorizationMonoid IsDedekindDomain IsDedekindDomain.He
 variable {R : Type _} [CommRing R] [IsDomain R] [IsDedekindDomain R] {K : Type _} [Field K]
   [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R)
 
+#print IsDedekindDomain.HeightOneSpectrum.maxPowDividing /-
 /-- Given a maximal ideal `v` and an ideal `I` of `R`, `max_pow_dividing` returns the maximal
   power of `v` dividing `I`. -/
 def IsDedekindDomain.HeightOneSpectrum.maxPowDividing (I : Ideal R) : Ideal R :=
   v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
 #align is_dedekind_domain.height_one_spectrum.max_pow_dividing IsDedekindDomain.HeightOneSpectrum.maxPowDividing
+-/
 
 /-- Only finitely many maximal ideals of `R` divide a given nonzero ideal. -/
 theorem Ideal.finite_factors {I : Ideal R} (hI : I ≠ 0) :
@@ -117,6 +119,7 @@ theorem finite_mulSupport_inv {I : Ideal R} (hI : I ≠ 0) :
   exact finite_mul_support_coe hI
 #align ideal.finite_mul_support_inv Ideal.finite_mulSupport_inv
 
+#print Ideal.finprod_not_dvd /-
 /-- For every nonzero ideal `I` of `v`, `v^(val_v(I) + 1)` does not divide `∏_v v^(val_v(I))`. -/
 theorem finprod_not_dvd (I : Ideal R) (hI : I ≠ 0) :
     ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
@@ -134,9 +137,11 @@ theorem finprod_not_dvd (I : Ideal R) (hI : I ≠ 0) :
   rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw 
   exact (finset.mem_erase.mp hw).1 (height_one_spectrum.ext w v (Eq.symm hvw))
 #align ideal.finprod_not_dvd Ideal.finprod_not_dvd
+-/
 
 end Ideal
 
+#print Associates.finprod_ne_zero /-
 theorem Associates.finprod_ne_zero (I : Ideal R) :
     Associates.mk (∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I) ≠ 0 :=
   by
@@ -147,9 +152,11 @@ theorem Associates.finprod_ne_zero (I : Ideal R) :
     apply pow_ne_zero _ v.ne_bot
   · exact one_ne_zero
 #align associates.finprod_ne_zero Associates.finprod_ne_zero
+-/
 
 namespace Ideal
 
+#print Ideal.finprod_count /-
 /-- The multiplicity of `v` in `∏_v v^(val_v(I))` equals `val_v(I)`. -/
 theorem finprod_count (I : Ideal R) (hI : I ≠ 0) :
     (Associates.mk v.asIdeal).count
@@ -166,6 +173,7 @@ theorem finprod_count (I : Ideal R) (hI : I ≠ 0) :
   rw [not_le] at h_not_dvd 
   apply Nat.eq_of_le_of_lt_succ h_dvd h_not_dvd
 #align ideal.finprod_count Ideal.finprod_count
+-/
 
 /-- The ideal `I` equals the finprod `∏_v v^(val_v(I))`. -/
 theorem finprod_heightOneSpectrum_factorization (I : Ideal R) (hI : I ≠ 0) :

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "2129f67f3b9e3b9e00088b260c75b762a9ff627f",
+    "rev": "328a56efb8ceb0f6f39c3b7b458b8351fac3847c",
     "name": "lean3port",
-    "inputRev?": "2129f67f3b9e3b9e00088b260c75b762a9ff627f"}},
+    "inputRev?": "328a56efb8ceb0f6f39c3b7b458b8351fac3847c"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "c340d9632c489054f7184276288307ef54d3514d",
+    "rev": "9f0fbd0c194939a5903ff92222095afc601abd26",
     "name": "mathlib",
-    "inputRev?": "c340d9632c489054f7184276288307ef54d3514d"}},
+    "inputRev?": "9f0fbd0c194939a5903ff92222095afc601abd26"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-06-11"
+def tag : String := "nightly-2023-06-06-13"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2129f67f3b9e3b9e00088b260c75b762a9ff627f"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"328a56efb8ceb0f6f39c3b7b458b8351fac3847c"
 
 @[default_target]
 lean_lib Mathbin where