bump to nightly-2023-03-01-03

mathlib commit leanprover-community/mathlib@4c586d2

Mathbin/Algebra/DualQuaternion.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module algebra.dual_quaternion
+! leanprover-community/mathlib commit 536c256e5de12c1dc0352b6b60b44f3c6c5ef340
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Algebra.DualNumber
+import Mathbin.Algebra.Quaternion
+
+/-!
+# Dual quaternions
+
+Similar to the way that rotations in 3D space can be represented by quaternions of unit length,
+rigid motions in 3D space can be represented by dual quaternions of unit length.
+
+## Main results
+
+* `quaternion.dual_number_equiv`: quaternions over dual numbers or dual
+  numbers over quaternions are equivalent constructions.
+
+## References
+
+* <https://en.wikipedia.org/wiki/Dual_quaternion>
+-/
+
+
+variable {R : Type _} [CommRing R]
+
+namespace Quaternion
+
+/-- The dual quaternions can be equivalently represented as a quaternion with dual coefficients,
+or as a dual number with quaternion coefficients.
+
+See also `matrix.dual_number_equiv` for a similar result. -/
+def dualNumberEquiv : Quaternion (DualNumber R) ≃ₐ[R] DualNumber (Quaternion R)
+    where
+  toFun q :=
+    (⟨q.re.fst, q.imI.fst, q.imJ.fst, q.imK.fst⟩, ⟨q.re.snd, q.imI.snd, q.imJ.snd, q.imK.snd⟩)
+  invFun d :=
+    ⟨(d.fst.re, d.snd.re), (d.fst.imI, d.snd.imI), (d.fst.imJ, d.snd.imJ), (d.fst.imK, d.snd.imK)⟩
+  left_inv := fun ⟨⟨r, rε⟩, ⟨i, iε⟩, ⟨j, jε⟩, ⟨k, kε⟩⟩ => rfl
+  right_inv := fun ⟨⟨r, i, j, k⟩, ⟨rε, iε, jε, kε⟩⟩ => rfl
+  map_mul' := by
+    rintro ⟨⟨xr, xrε⟩, ⟨xi, xiε⟩, ⟨xj, xjε⟩, ⟨xk, xkε⟩⟩
+    rintro ⟨⟨yr, yrε⟩, ⟨yi, yiε⟩, ⟨yj, yjε⟩, ⟨yk, ykε⟩⟩
+    ext : 1
+    · rfl
+    · dsimp
+      congr 1 <;> ring
+  map_add' := by
+    rintro ⟨⟨xr, xrε⟩, ⟨xi, xiε⟩, ⟨xj, xjε⟩, ⟨xk, xkε⟩⟩
+    rintro ⟨⟨yr, yrε⟩, ⟨yi, yiε⟩, ⟨yj, yjε⟩, ⟨yk, ykε⟩⟩
+    rfl
+  commutes' r := rfl
+#align quaternion.dual_number_equiv Quaternion.dualNumberEquiv
+
+/-! Lemmas characterizing `quaternion.dual_number_equiv`. -/
+
+
+-- `simps` can't work on `dual_number` because it's not a structure
+@[simp]
+theorem re_fst_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).fst.re = q.re.fst :=
+  rfl
+#align quaternion.re_fst_dual_number_equiv Quaternion.re_fst_dualNumberEquiv
+
+@[simp]
+theorem imI_fst_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).fst.imI = q.imI.fst :=
+  rfl
+#align quaternion.im_i_fst_dual_number_equiv Quaternion.imI_fst_dualNumberEquiv
+
+@[simp]
+theorem imJ_fst_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).fst.imJ = q.imJ.fst :=
+  rfl
+#align quaternion.im_j_fst_dual_number_equiv Quaternion.imJ_fst_dualNumberEquiv
+
+@[simp]
+theorem imK_fst_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).fst.imK = q.imK.fst :=
+  rfl
+#align quaternion.im_k_fst_dual_number_equiv Quaternion.imK_fst_dualNumberEquiv
+
+@[simp]
+theorem re_snd_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).snd.re = q.re.snd :=
+  rfl
+#align quaternion.re_snd_dual_number_equiv Quaternion.re_snd_dualNumberEquiv
+
+@[simp]
+theorem imI_snd_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).snd.imI = q.imI.snd :=
+  rfl
+#align quaternion.im_i_snd_dual_number_equiv Quaternion.imI_snd_dualNumberEquiv
+
+@[simp]
+theorem imJ_snd_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).snd.imJ = q.imJ.snd :=
+  rfl
+#align quaternion.im_j_snd_dual_number_equiv Quaternion.imJ_snd_dualNumberEquiv
+
+@[simp]
+theorem imK_snd_dualNumberEquiv (q : Quaternion (DualNumber R)) :
+    (dualNumberEquiv q).snd.imK = q.imK.snd :=
+  rfl
+#align quaternion.im_k_snd_dual_number_equiv Quaternion.imK_snd_dualNumberEquiv
+
+@[simp]
+theorem fst_re_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).re.fst = d.fst.re :=
+  rfl
+#align quaternion.fst_re_dual_number_equiv_symm Quaternion.fst_re_dualNumberEquiv_symm
+
+@[simp]
+theorem fst_imI_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).imI.fst = d.fst.imI :=
+  rfl
+#align quaternion.fst_im_i_dual_number_equiv_symm Quaternion.fst_imI_dualNumberEquiv_symm
+
+@[simp]
+theorem fst_imJ_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).imJ.fst = d.fst.imJ :=
+  rfl
+#align quaternion.fst_im_j_dual_number_equiv_symm Quaternion.fst_imJ_dualNumberEquiv_symm
+
+@[simp]
+theorem fst_imK_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).imK.fst = d.fst.imK :=
+  rfl
+#align quaternion.fst_im_k_dual_number_equiv_symm Quaternion.fst_imK_dualNumberEquiv_symm
+
+@[simp]
+theorem snd_re_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).re.snd = d.snd.re :=
+  rfl
+#align quaternion.snd_re_dual_number_equiv_symm Quaternion.snd_re_dualNumberEquiv_symm
+
+@[simp]
+theorem snd_imI_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).imI.snd = d.snd.imI :=
+  rfl
+#align quaternion.snd_im_i_dual_number_equiv_symm Quaternion.snd_imI_dualNumberEquiv_symm
+
+@[simp]
+theorem snd_imJ_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).imJ.snd = d.snd.imJ :=
+  rfl
+#align quaternion.snd_im_j_dual_number_equiv_symm Quaternion.snd_imJ_dualNumberEquiv_symm
+
+@[simp]
+theorem snd_imK_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) :
+    (dualNumberEquiv.symm d).imK.snd = d.snd.imK :=
+  rfl
+#align quaternion.snd_im_k_dual_number_equiv_symm Quaternion.snd_imK_dualNumberEquiv_symm
+
+end Quaternion
+

Mathbin/Algebra/Order/AbsoluteValue.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.order.absolute_value
-! leanprover-community/mathlib commit 7ea604785a41a0681eac70c5a82372493dbefc68
+! leanprover-community/mathlib commit e1a7bdeb4fd826b7e71d130d34988f0a2d26a177
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -47,8 +47,6 @@ namespace AbsoluteValue
 
 attribute [nolint doc_blame] AbsoluteValue.toMulHom
 
-initialize_simps_projections AbsoluteValue (to_mul_hom_to_fun → apply)
-
 section OrderedSemiring
 
 section Semiring
@@ -123,6 +121,15 @@ theorem ext ⦃f g : AbsoluteValue R S⦄ : (∀ x, f x = g x) → f = g :=
   FunLike.ext _ _
 #align absolute_value.ext AbsoluteValue.ext
 
+#print AbsoluteValue.Simps.apply /-
+/-- See Note [custom simps projection]. -/
+def Simps.apply (f : AbsoluteValue R S) : R → S :=
+  f
+#align absolute_value.simps.apply AbsoluteValue.Simps.apply
+-/
+
+initialize_simps_projections AbsoluteValue (to_mul_hom_to_fun → apply)
+
 /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
 directly. -/
 instance : CoeFun (AbsoluteValue R S) fun f => R → S :=

Mathbin/All.lean

@@ -123,6 +123,7 @@ import Mathbin.Algebra.DirectSum.Ring
 import Mathbin.Algebra.Divisibility.Basic
 import Mathbin.Algebra.Divisibility.Units
 import Mathbin.Algebra.DualNumber
+import Mathbin.Algebra.DualQuaternion
 import Mathbin.Algebra.EuclideanDomain.Basic
 import Mathbin.Algebra.EuclideanDomain.Defs
 import Mathbin.Algebra.EuclideanDomain.Instances
@@ -685,6 +686,7 @@ import Mathbin.Analysis.NormedSpace.Ray
 import Mathbin.Analysis.NormedSpace.RieszLemma
 import Mathbin.Analysis.NormedSpace.Spectrum
 import Mathbin.Analysis.NormedSpace.Star.Basic
+import Mathbin.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus
 import Mathbin.Analysis.NormedSpace.Star.Exponential
 import Mathbin.Analysis.NormedSpace.Star.GelfandDuality
 import Mathbin.Analysis.NormedSpace.Star.Matrix
@@ -1138,6 +1140,7 @@ import Mathbin.Combinatorics.SimpleGraph.DegreeSum
 import Mathbin.Combinatorics.SimpleGraph.Density
 import Mathbin.Combinatorics.SimpleGraph.Ends.Defs
 import Mathbin.Combinatorics.SimpleGraph.Ends.Properties
+import Mathbin.Combinatorics.SimpleGraph.Finsubgraph
 import Mathbin.Combinatorics.SimpleGraph.Hasse
 import Mathbin.Combinatorics.SimpleGraph.IncMatrix
 import Mathbin.Combinatorics.SimpleGraph.Matching

Mathbin/Analysis/InnerProductSpace/TwoDim.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 
 ! This file was ported from Lean 3 source module analysis.inner_product_space.two_dim
-! leanprover-community/mathlib commit e99e8c8934985b3bed8c6badbd333043a18c49c9
+! leanprover-community/mathlib commit e65771194f9e923a70dfb49b6ca7be6e400d8b6f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -470,16 +470,14 @@ theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) :
     let b : ℝ := (o.basis_right_angle_rotation x hx).repr y 1
     suffices 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x)
       by
-      -- TODO trace the `dsimp` lemmas in this block to make a single `simp only`
       rw [← (o.basis_right_angle_rotation x hx).sum_repr y]
-      simp only [Fin.sum_univ_succ, coe_basis_right_angle_rotation]
-      dsimp
-      simp only [o.area_form_apply_self, map_smul, map_add, map_zero, inner_smul_left,
-        inner_smul_right, inner_add_left, inner_add_right, inner_zero_right, LinearMap.add_apply,
-        Matrix.cons_val_one]
-      dsimp
-      simp only [o.area_form_right_angle_rotation_right, mul_zero, add_zero, zero_add, neg_zero,
-        o.inner_right_angle_rotation_right, o.area_form_apply_self, real_inner_self_eq_norm_sq]
+      simp only [Fin.sum_univ_succ, coe_basis_right_angle_rotation, Matrix.cons_val_zero,
+        Fin.succ_zero_eq_one', Fintype.univ_of_isEmpty, Finset.sum_empty, o.area_form_apply_self,
+        map_smul, map_add, map_zero, inner_smul_left, inner_smul_right, inner_add_left,
+        inner_add_right, inner_zero_right, LinearMap.add_apply, Matrix.cons_val_one,
+        Matrix.head_cons, Algebra.id.smul_eq_mul, o.area_form_right_angle_rotation_right, mul_zero,
+        add_zero, zero_add, neg_zero, o.inner_right_angle_rotation_right, o.area_form_apply_self,
+        real_inner_self_eq_norm_sq]
       exact this
     rintro ⟨ha, hb⟩
     have hx' : 0 < ‖x‖ := by simpa using hx

Mathbin/Analysis/NormedSpace/Star/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 
 ! This file was ported from Lean 3 source module analysis.normed_space.star.basic
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit e65771194f9e923a70dfb49b6ca7be6e400d8b6f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,7 @@ import Mathbin.Analysis.NormedSpace.Basic
 import Mathbin.Analysis.NormedSpace.LinearIsometry
 import Mathbin.Algebra.Star.SelfAdjoint
 import Mathbin.Algebra.Star.Unitary
+import Mathbin.Topology.Algebra.StarSubalgebra
 
 /-!
 # Normed star rings and algebras
@@ -321,3 +322,17 @@ theorem starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x :=
 
 end starₗᵢ
 
+namespace StarSubalgebra
+
+instance toNormedAlgebra {𝕜 A : Type _} [NormedField 𝕜] [StarRing 𝕜] [SemiNormedRing A] [StarRing A]
+    [NormedAlgebra 𝕜 A] [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) : NormedAlgebra 𝕜 S :=
+  @NormedAlgebra.induced _ 𝕜 S A _ (SubringClass.toRing S) S.Algebra _ _ _ S.Subtype
+#align star_subalgebra.to_normed_algebra StarSubalgebra.toNormedAlgebra
+
+instance to_cstarRing {R A} [CommRing R] [StarRing R] [NormedRing A] [StarRing A] [CstarRing A]
+    [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) : CstarRing S
+    where norm_star_mul_self x := @CstarRing.norm_star_mul_self A _ _ _ x
+#align star_subalgebra.to_cstar_ring StarSubalgebra.to_cstarRing
+
+end StarSubalgebra
+