bump to nightly-2023-04-04-14

mathlib commit leanprover-community/mathlib@3cacc94

Mathbin/Algebra/Lie/Classical.lean

@@ -115,7 +115,7 @@ basis of sl n R. -/
 def eb (h : j ≠ i) : sl n R :=
   ⟨Matrix.stdBasisMatrix i j (1 : R),
     show Matrix.stdBasisMatrix i j (1 : R) ∈ LinearMap.ker (Matrix.traceLinearMap n R R) from
-      Matrix.stdBasisMatrix.trace_zero i j (1 : R) h⟩
+      Matrix.StdBasisMatrix.trace_zero i j (1 : R) h⟩
 #align lie_algebra.special_linear.Eb LieAlgebra.SpecialLinear.eb
 
 @[simp]

Mathbin/Algebra/Squarefree.lean

@@ -376,12 +376,24 @@ end UniqueFactorizationMonoid
 
 namespace Int
 
+/- warning: int.squarefree_nat_abs -> Int.squarefree_natAbs is a dubious translation:
+lean 3 declaration is
+  forall {n : Int}, Iff (Squarefree.{0} Nat Nat.monoid (Int.natAbs n)) (Squarefree.{0} Int Int.monoid n)
+but is expected to have type
+  forall {n : Int}, Iff (Squarefree.{0} Nat Nat.monoid (Int.natAbs n)) (Squarefree.{0} Int Int.instMonoidInt n)
+Case conversion may be inaccurate. Consider using '#align int.squarefree_nat_abs Int.squarefree_natAbsₓ'. -/
 @[simp]
 theorem squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n := by
   simp_rw [Squarefree, nat_abs_surjective.forall, ← nat_abs_mul, nat_abs_dvd_iff_dvd,
     is_unit_iff_nat_abs_eq, Nat.isUnit_iff]
 #align int.squarefree_nat_abs Int.squarefree_natAbs
 
+/- warning: int.squarefree_coe_nat -> Int.squarefree_coe_nat is a dubious translation:
+lean 3 declaration is
+  forall {n : Nat}, Iff (Squarefree.{0} Int Int.monoid ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) n)) (Squarefree.{0} Nat Nat.monoid n)
+but is expected to have type
+  forall {n : Nat}, Iff (Squarefree.{0} Int Int.instMonoidInt (Nat.cast.{0} Int instNatCastInt n)) (Squarefree.{0} Nat Nat.monoid n)
+Case conversion may be inaccurate. Consider using '#align int.squarefree_coe_nat Int.squarefree_coe_natₓ'. -/
 @[simp]
 theorem squarefree_coe_nat {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n := by
   rw [← squarefree_nat_abs, nat_abs_of_nat]

Mathbin/Data/Int/Basic.lean

@@ -374,8 +374,10 @@ variable {a b : ℤ} {n : ℕ}
 
 attribute [simp] nat_abs_of_nat nat_abs_zero nat_abs_one
 
+#print Int.natAbs_surjective /-
 theorem natAbs_surjective : natAbs.Surjective := fun n => ⟨n, natAbs_ofNat n⟩
 #align int.nat_abs_surjective Int.natAbs_surjective
+-/
 
 #print Int.natAbs_add_le /-
 theorem natAbs_add_le (a b : ℤ) : natAbs (a + b) ≤ natAbs a + natAbs b :=

Mathbin/Data/Matrix/CharP.lean

@@ -20,6 +20,12 @@ open Matrix
 
 variable {n : Type _} [Fintype n] {R : Type _} [Ring R]
 
+/- warning: matrix.char_p -> Matrix.charP is a dubious translation:
+lean 3 declaration is
+  forall {n : Type.{u1}} [_inst_1 : Fintype.{u1} n] {R : Type.{u2}} [_inst_2 : Ring.{u2} R] [_inst_3 : DecidableEq.{succ u1} n] [_inst_4 : Nonempty.{succ u1} n] (p : Nat) [_inst_5 : CharP.{u2} R (AddGroupWithOne.toAddMonoidWithOne.{u2} R (AddCommGroupWithOne.toAddGroupWithOne.{u2} R (Ring.toAddCommGroupWithOne.{u2} R _inst_2))) p], CharP.{max u1 u2} (Matrix.{u1, u1, u2} n n R) (AddGroupWithOne.toAddMonoidWithOne.{max u1 u2} (Matrix.{u1, u1, u2} n n R) (AddCommGroupWithOne.toAddGroupWithOne.{max u1 u2} (Matrix.{u1, u1, u2} n n R) (Ring.toAddCommGroupWithOne.{max u1 u2} (Matrix.{u1, u1, u2} n n R) (Matrix.ring.{u2, u1} n R _inst_1 (fun (a : n) (b : n) => _inst_3 a b) _inst_2)))) p
+but is expected to have type
+  forall {n : Type.{u1}} [_inst_1 : Fintype.{u1} n] {R : Type.{u2}} [_inst_2 : Ring.{u2} R] [_inst_3 : DecidableEq.{succ u1} n] [_inst_4 : Nonempty.{succ u1} n] (p : Nat) [_inst_5 : CharP.{u2} R (AddGroupWithOne.toAddMonoidWithOne.{u2} R (Ring.toAddGroupWithOne.{u2} R _inst_2)) p], CharP.{max u2 u1} (Matrix.{u1, u1, u2} n n R) (AddGroupWithOne.toAddMonoidWithOne.{max u1 u2} (Matrix.{u1, u1, u2} n n R) (Ring.toAddGroupWithOne.{max u1 u2} (Matrix.{u1, u1, u2} n n R) (Matrix.instRingMatrix.{u2, u1} n R _inst_1 (fun (a : n) (b : n) => _inst_3 a b) _inst_2))) p
+Case conversion may be inaccurate. Consider using '#align matrix.char_p Matrix.charPₓ'. -/
 instance Matrix.charP [DecidableEq n] [Nonempty n] (p : ℕ) [CharP R p] : CharP (Matrix n n R) p :=
   ⟨by
     intro k

Mathbin/LinearAlgebra/Matrix/Orthogonal.lean

@@ -38,25 +38,41 @@ variable (A : Matrix m n α)
 
 open Matrix
 
+#print Matrix.HasOrthogonalRows /-
 /-- `A.has_orthogonal_rows` means matrix `A` has orthogonal rows (with respect to
 `matrix.dot_product`). -/
 def HasOrthogonalRows [Fintype n] : Prop :=
   ∀ ⦃i₁ i₂⦄, i₁ ≠ i₂ → dotProduct (A i₁) (A i₂) = 0
 #align matrix.has_orthogonal_rows Matrix.HasOrthogonalRows
+-/
 
+#print Matrix.HasOrthogonalCols /-
 /-- `A.has_orthogonal_rows` means matrix `A` has orthogonal columns (with respect to
 `matrix.dot_product`). -/
 def HasOrthogonalCols [Fintype m] : Prop :=
   HasOrthogonalRows Aᵀ
 #align matrix.has_orthogonal_cols Matrix.HasOrthogonalCols
+-/
 
+/- warning: matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols -> Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {n : Type.{u2}} {m : Type.{u3}} [_inst_1 : Mul.{u1} α] [_inst_2 : AddCommMonoid.{u1} α] (A : Matrix.{u3, u2, u1} m n α) [_inst_3 : Fintype.{u3} m], Iff (Matrix.HasOrthogonalRows.{u1, u3, u2} α m n _inst_1 _inst_2 (Matrix.transpose.{u1, u3, u2} m n α A) _inst_3) (Matrix.HasOrthogonalCols.{u1, u2, u3} α n m _inst_1 _inst_2 A _inst_3)
+but is expected to have type
+  forall {α : Type.{u2}} {n : Type.{u1}} {m : Type.{u3}} [_inst_1 : Mul.{u2} α] [_inst_2 : AddCommMonoid.{u2} α] (A : Matrix.{u3, u1, u2} m n α) [_inst_3 : Fintype.{u3} m], Iff (Matrix.HasOrthogonalRows.{u2, u3, u1} α m n _inst_1 _inst_2 (Matrix.transpose.{u2, u3, u1} m n α A) _inst_3) (Matrix.HasOrthogonalCols.{u2, u1, u3} α n m _inst_1 _inst_2 A _inst_3)
+Case conversion may be inaccurate. Consider using '#align matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalColsₓ'. -/
 /-- `Aᵀ` has orthogonal rows iff `A` has orthogonal columns. -/
 @[simp]
 theorem transpose_hasOrthogonalRows_iff_hasOrthogonalCols [Fintype m] :
     Aᵀ.HasOrthogonalRows ↔ A.HasOrthogonalCols :=
   Iff.rfl
 #align matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols
 
+/- warning: matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows -> Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {n : Type.{u2}} {m : Type.{u3}} [_inst_1 : Mul.{u1} α] [_inst_2 : AddCommMonoid.{u1} α] (A : Matrix.{u3, u2, u1} m n α) [_inst_3 : Fintype.{u2} n], Iff (Matrix.HasOrthogonalCols.{u1, u3, u2} α m n _inst_1 _inst_2 (Matrix.transpose.{u1, u3, u2} m n α A) _inst_3) (Matrix.HasOrthogonalRows.{u1, u2, u3} α n m _inst_1 _inst_2 A _inst_3)
+but is expected to have type
+  forall {α : Type.{u2}} {n : Type.{u3}} {m : Type.{u1}} [_inst_1 : Mul.{u2} α] [_inst_2 : AddCommMonoid.{u2} α] (A : Matrix.{u1, u3, u2} m n α) [_inst_3 : Fintype.{u3} n], Iff (Matrix.HasOrthogonalCols.{u2, u1, u3} α m n _inst_1 _inst_2 (Matrix.transpose.{u2, u1, u3} m n α A) _inst_3) (Matrix.HasOrthogonalRows.{u2, u3, u1} α n m _inst_1 _inst_2 A _inst_3)
+Case conversion may be inaccurate. Consider using '#align matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRowsₓ'. -/
 /-- `Aᵀ` has orthogonal columns iff `A` has orthogonal rows. -/
 @[simp]
 theorem transpose_hasOrthogonalCols_iff_hasOrthogonalRows [Fintype n] :
@@ -66,21 +82,45 @@ theorem transpose_hasOrthogonalCols_iff_hasOrthogonalRows [Fintype n] :
 
 variable {A}
 
+/- warning: matrix.has_orthogonal_rows.has_orthogonal_cols -> Matrix.HasOrthogonalRows.hasOrthogonalCols is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {n : Type.{u2}} {m : Type.{u3}} [_inst_1 : Mul.{u1} α] [_inst_2 : AddCommMonoid.{u1} α] {A : Matrix.{u3, u2, u1} m n α} [_inst_3 : Fintype.{u3} m], (Matrix.HasOrthogonalRows.{u1, u3, u2} α m n _inst_1 _inst_2 (Matrix.transpose.{u1, u3, u2} m n α A) _inst_3) -> (Matrix.HasOrthogonalCols.{u1, u2, u3} α n m _inst_1 _inst_2 A _inst_3)
+but is expected to have type
+  forall {α : Type.{u2}} {n : Type.{u1}} {m : Type.{u3}} [_inst_1 : Mul.{u2} α] [_inst_2 : AddCommMonoid.{u2} α] {A : Matrix.{u3, u1, u2} m n α} [_inst_3 : Fintype.{u3} m], (Matrix.HasOrthogonalRows.{u2, u3, u1} α m n _inst_1 _inst_2 (Matrix.transpose.{u2, u3, u1} m n α A) _inst_3) -> (Matrix.HasOrthogonalCols.{u2, u1, u3} α n m _inst_1 _inst_2 A _inst_3)
+Case conversion may be inaccurate. Consider using '#align matrix.has_orthogonal_rows.has_orthogonal_cols Matrix.HasOrthogonalRows.hasOrthogonalColsₓ'. -/
 theorem HasOrthogonalRows.hasOrthogonalCols [Fintype m] (h : Aᵀ.HasOrthogonalRows) :
     A.HasOrthogonalCols :=
   h
 #align matrix.has_orthogonal_rows.has_orthogonal_cols Matrix.HasOrthogonalRows.hasOrthogonalCols
 
+/- warning: matrix.has_orthogonal_cols.transpose_has_orthogonal_rows -> Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {n : Type.{u2}} {m : Type.{u3}} [_inst_1 : Mul.{u1} α] [_inst_2 : AddCommMonoid.{u1} α] {A : Matrix.{u3, u2, u1} m n α} [_inst_3 : Fintype.{u3} m], (Matrix.HasOrthogonalCols.{u1, u2, u3} α n m _inst_1 _inst_2 A _inst_3) -> (Matrix.HasOrthogonalRows.{u1, u3, u2} α m n _inst_1 _inst_2 (Matrix.transpose.{u1, u3, u2} m n α A) _inst_3)
+but is expected to have type
+  forall {α : Type.{u2}} {n : Type.{u1}} {m : Type.{u3}} [_inst_1 : Mul.{u2} α] [_inst_2 : AddCommMonoid.{u2} α] {A : Matrix.{u3, u1, u2} m n α} [_inst_3 : Fintype.{u3} m], (Matrix.HasOrthogonalCols.{u2, u1, u3} α n m _inst_1 _inst_2 A _inst_3) -> (Matrix.HasOrthogonalRows.{u2, u3, u1} α m n _inst_1 _inst_2 (Matrix.transpose.{u2, u3, u1} m n α A) _inst_3)
+Case conversion may be inaccurate. Consider using '#align matrix.has_orthogonal_cols.transpose_has_orthogonal_rows Matrix.HasOrthogonalCols.transpose_hasOrthogonalRowsₓ'. -/
 theorem HasOrthogonalCols.transpose_hasOrthogonalRows [Fintype m] (h : A.HasOrthogonalCols) :
     Aᵀ.HasOrthogonalRows :=
   h
 #align matrix.has_orthogonal_cols.transpose_has_orthogonal_rows Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows
 
+/- warning: matrix.has_orthogonal_cols.has_orthogonal_rows -> Matrix.HasOrthogonalCols.hasOrthogonalRows is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {n : Type.{u2}} {m : Type.{u3}} [_inst_1 : Mul.{u1} α] [_inst_2 : AddCommMonoid.{u1} α] {A : Matrix.{u3, u2, u1} m n α} [_inst_3 : Fintype.{u2} n], (Matrix.HasOrthogonalCols.{u1, u3, u2} α m n _inst_1 _inst_2 (Matrix.transpose.{u1, u3, u2} m n α A) _inst_3) -> (Matrix.HasOrthogonalRows.{u1, u2, u3} α n m _inst_1 _inst_2 A _inst_3)
+but is expected to have type
+  forall {α : Type.{u2}} {n : Type.{u3}} {m : Type.{u1}} [_inst_1 : Mul.{u2} α] [_inst_2 : AddCommMonoid.{u2} α] {A : Matrix.{u1, u3, u2} m n α} [_inst_3 : Fintype.{u3} n], (Matrix.HasOrthogonalCols.{u2, u1, u3} α m n _inst_1 _inst_2 (Matrix.transpose.{u2, u1, u3} m n α A) _inst_3) -> (Matrix.HasOrthogonalRows.{u2, u3, u1} α n m _inst_1 _inst_2 A _inst_3)
+Case conversion may be inaccurate. Consider using '#align matrix.has_orthogonal_cols.has_orthogonal_rows Matrix.HasOrthogonalCols.hasOrthogonalRowsₓ'. -/
 theorem HasOrthogonalCols.hasOrthogonalRows [Fintype n] (h : Aᵀ.HasOrthogonalCols) :
     A.HasOrthogonalRows :=
   h
 #align matrix.has_orthogonal_cols.has_orthogonal_rows Matrix.HasOrthogonalCols.hasOrthogonalRows
 
+/- warning: matrix.has_orthogonal_rows.transpose_has_orthogonal_cols -> Matrix.HasOrthogonalRows.transpose_hasOrthogonalCols is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {n : Type.{u2}} {m : Type.{u3}} [_inst_1 : Mul.{u1} α] [_inst_2 : AddCommMonoid.{u1} α] {A : Matrix.{u3, u2, u1} m n α} [_inst_3 : Fintype.{u2} n], (Matrix.HasOrthogonalRows.{u1, u2, u3} α n m _inst_1 _inst_2 A _inst_3) -> (Matrix.HasOrthogonalCols.{u1, u3, u2} α m n _inst_1 _inst_2 (Matrix.transpose.{u1, u3, u2} m n α A) _inst_3)
+but is expected to have type
+  forall {α : Type.{u2}} {n : Type.{u3}} {m : Type.{u1}} [_inst_1 : Mul.{u2} α] [_inst_2 : AddCommMonoid.{u2} α] {A : Matrix.{u1, u3, u2} m n α} [_inst_3 : Fintype.{u3} n], (Matrix.HasOrthogonalRows.{u2, u3, u1} α n m _inst_1 _inst_2 A _inst_3) -> (Matrix.HasOrthogonalCols.{u2, u1, u3} α m n _inst_1 _inst_2 (Matrix.transpose.{u2, u1, u3} m n α A) _inst_3)
+Case conversion may be inaccurate. Consider using '#align matrix.has_orthogonal_rows.transpose_has_orthogonal_cols Matrix.HasOrthogonalRows.transpose_hasOrthogonalColsₓ'. -/
 theorem HasOrthogonalRows.transpose_hasOrthogonalCols [Fintype n] (h : A.HasOrthogonalRows) :
     Aᵀ.HasOrthogonalCols :=
   h