diff --git a/Mathlib.lean b/Mathlib.lean index 91950c57318e2..a90654627d681 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -375,6 +375,7 @@ import Mathlib.Algebra.Star.BigOperators import Mathlib.Algebra.Star.CHSH import Mathlib.Algebra.Star.Free import Mathlib.Algebra.Star.Module +import Mathlib.Algebra.Star.Order import Mathlib.Algebra.Star.Pi import Mathlib.Algebra.Star.Pointwise import Mathlib.Algebra.Star.Prod diff --git a/Mathlib/Algebra/MonoidAlgebra/Grading.lean b/Mathlib/Algebra/MonoidAlgebra/Grading.lean index f406a2a1c552d..6cb4319dc3001 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Grading.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Grading.lean @@ -123,7 +123,7 @@ instance grade.gradedMonoid [AddMonoid M] [CommSemiring R] : variable [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) -set_option maxHeartbeats 250000 in +set_option maxHeartbeats 260000 in /-- Auxiliary definition; the canonical grade decomposition, used to provide `DirectSum.decompose`. -/ def decomposeAux : AddMonoidAlgebra R M →ₐ[R] ⨁ i : ι, gradeBy R f i := diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean index ddbba7ee3e855..bc67ab8d98e93 100644 --- a/Mathlib/Algebra/Star/Basic.lean +++ b/Mathlib/Algebra/Star/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison ! This file was ported from Lean 3 source module algebra.star.basic -! leanprover-community/mathlib commit dc7ac07acd84584426773e69e51035bea9a770e7 +! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -24,23 +24,12 @@ These are implemented as "mixin" typeclasses, so to summon a star ring (for exam one needs to write `(R : Type _) [Ring R] [StarRing R]`. This avoids difficulties with diamond inheritance. -We also define the class `StarOrderedRing R`, which says that the order on `R` respects the -star operation, i.e. an element `r` is nonnegative iff there exists an `s` such that -`r = star s * s`. - For now we simply do not introduce notations, as different users are expected to feel strongly about the relative merits of `r^*`, `r†`, `rᘁ`, and so on. Our star rings are actually star semirings, but of course we can prove `star_neg : star (-r) = - star r` when the underlying semiring is a ring. - -## TODO - -* In a Banach star algebra without a well-defined square root, the natural ordering is given by the -positive cone which is the closure of the sums of elements `star r * r`. A weaker version of -`StarOrderedRing` could be defined for this case. Note that the current definition has the -advantage of not requiring a topology. -/ assert_not_exists Finset @@ -485,71 +474,6 @@ def starRingOfComm {R : Type _} [CommSemiring R] : StarRing R := star_add := fun _ _ => rfl } #align star_ring_of_comm starRingOfComm -/-- An ordered `*`-ring is a ring which is both an `OrderedAddCommGroup` and a `*`-ring, -and `0 ≤ r ↔ ∃ s, r = star s * s`. --/ -class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] extends StarRing R where - /-- addition commutes with `≤` -/ - add_le_add_left : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b - /--characterization of non-negativity -/ - nonneg_iff : ∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s -#align star_ordered_ring StarOrderedRing - -namespace StarOrderedRing - --- see note [lower instance priority] -instance (priority := 100) [NonUnitalRing R] [PartialOrder R] [StarOrderedRing R] : - OrderedAddCommGroup R := - { inferInstanceAs (NonUnitalRing R), inferInstanceAs (PartialOrder R), - inferInstanceAs (StarOrderedRing R) with } - -end StarOrderedRing - -section NonUnitalSemiring - -variable [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] - -theorem star_mul_self_nonneg {r : R} : 0 ≤ star r * r := - (StarOrderedRing.nonneg_iff _).mpr ⟨r, rfl⟩ -#align star_mul_self_nonneg star_mul_self_nonneg - -theorem star_mul_self_nonneg' {r : R} : 0 ≤ r * star r := by - have : r * star r = star (star r) * star r := by simp only [star_star] - rw [this] - exact star_mul_self_nonneg -#align star_mul_self_nonneg' star_mul_self_nonneg' - -theorem conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c := by - obtain ⟨x, h⟩ := (StarOrderedRing.nonneg_iff _).1 ha - apply (StarOrderedRing.nonneg_iff _).2 - exists x * c - simp only [h, star_mul, ← mul_assoc] -#align conjugate_nonneg conjugate_nonneg - -theorem conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c := by - simpa only [star_star] using conjugate_nonneg ha (star c) -#align conjugate_nonneg' conjugate_nonneg' - -end NonUnitalSemiring - -section NonUnitalRing - -variable [NonUnitalRing R] [PartialOrder R] [StarOrderedRing R] - -theorem conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : - star c * a * c ≤ star c * b * c := by - rw [← sub_nonneg] at hab⊢ - convert conjugate_nonneg hab c using 1 - simp only [mul_sub, sub_mul] -#align conjugate_le_conjugate conjugate_le_conjugate - -theorem conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : - c * a * star c ≤ c * b * star c := by - simpa only [star_star] using conjugate_le_conjugate hab (star c) -#align conjugate_le_conjugate' conjugate_le_conjugate' - -end NonUnitalRing - /-- A star module `A` over a star ring `R` is a module which is a star add monoid, and the two star structures are compatible in the sense `star (r • a) = star r • star a`. diff --git a/Mathlib/Algebra/Star/CHSH.lean b/Mathlib/Algebra/Star/CHSH.lean index 695aeefb8bea4..8870b59946b76 100644 --- a/Mathlib/Algebra/Star/CHSH.lean +++ b/Mathlib/Algebra/Star/CHSH.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison ! This file was ported from Lean 3 source module algebra.star.chsh -! leanprover-community/mathlib commit 468b141b14016d54b479eb7a0fff1e360b7e3cf6 +! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -143,7 +143,7 @@ theorem CHSH_inequality_of_comm [OrderedCommRing R] [StarOrderedRing R] [Algebra arg 2 arg 1 rw [← sa] - convert smul_le_smul_of_nonneg (R := ℝ) (star_mul_self_nonneg : 0 ≤ star P * P) _ + convert smul_le_smul_of_nonneg (R := ℝ) (star_mul_self_nonneg P) _ · simp · norm_num apply le_of_sub_nonneg @@ -235,7 +235,7 @@ theorem tsirelson_inequality [OrderedRing R] [StarOrderedRing R] [Algebra ℝ R] skip congr rw [← P_sa] - convert(star_mul_self_nonneg : 0 ≤ star P * P) + convert (star_mul_self_nonneg P) have Q2_nonneg : 0 ≤ Q ^ 2 := by rw [sq] conv => @@ -243,7 +243,7 @@ theorem tsirelson_inequality [OrderedRing R] [StarOrderedRing R] [Algebra ℝ R] skip congr rw [← Q_sa] - convert(star_mul_self_nonneg : 0 ≤ star Q * Q) + convert (star_mul_self_nonneg Q) convert smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg) (le_of_lt (show 0 < √2⁻¹ by norm_num)) -- `norm_num` can't directly show `0 ≤ √2⁻¹` diff --git a/Mathlib/Algebra/Star/Order.lean b/Mathlib/Algebra/Star/Order.lean new file mode 100644 index 0000000000000..af81f7273058e --- /dev/null +++ b/Mathlib/Algebra/Star/Order.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2023 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison + +! This file was ported from Lean 3 source module algebra.star.order +! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Algebra.Star.Basic +import Mathlib.GroupTheory.Submonoid.Basic + +/-! # Star ordered rings + +We define the class `StarOrderedRing R`, which says that the order on `R` respects the +star operation, i.e. an element `r` is nonnegative iff it is in the `AddSubmonoid` generated by +elements of the form `star s * s`. In many cases, including all C⋆-algebras, this can be reduced to +`0 ≤ r ↔ ∃ s, r = star s * s`. However, this generality is slightly more convenient (e.g., it +allows us to register a `StarOrderedRing` instance for `ℚ`), and more closely resembles the +literature (see the seminal paper [*The positive cone in Banach algebras*][kelleyVaught1953]) + +In order to accodomate `NonUnitalSemiring R`, we actually don't characterize nonnegativity, but +rather the entire `≤` relation with `StarOrderedRing.le_iff`. However, notice that when `R` is a +`NonUnitalRing`, these are equivalent (see `StarOrderedRing.nonneg_iff` and +`StarOrderedRing.ofNonnegIff`). + +## TODO + +* In a Banach star algebra without a well-defined square root, the natural ordering is given by the +positive cone which is the _closure_ of the sums of elements `star r * r`. A weaker version of +`StarOrderedRing` could be defined for this case (again, see +[*The positive cone in Banach algebras*][kelleyVaught1953]). Note that the current definition has +the advantage of not requiring a topology. +-/ + + +universe u + +variable {R : Type u} + +/-- An ordered `*`-ring is a ring which is both an `OrderedAddCommGroup` and a `*`-ring, +and the nonnegative elements constitute precisely the `AddSubmonoid` generated by +elements of the form `star s * s`. + +If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, it may be more +convenient to declare instances using `StarOrderedRing.ofNonnegIff'`. -/ +class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] extends StarRing R where + /-- addition commutes with `≤` -/ + add_le_add_left : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b + /-- characterization of the order in terms of the `StarRing` structure. -/ + le_iff : + ∀ x y : R, x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p +#align star_ordered_ring StarOrderedRing + +namespace StarOrderedRing + +-- see note [lower instance priority] +instance (priority := 100) toOrderedAddCommMonoid [NonUnitalSemiring R] [PartialOrder R] + [StarOrderedRing R] : OrderedAddCommMonoid R := + { show NonUnitalSemiring R by infer_instance, show PartialOrder R by infer_instance, + show StarOrderedRing R by infer_instance with } +#align star_ordered_ring.to_ordered_add_comm_monoid StarOrderedRing.toOrderedAddCommMonoid + +-- see note [lower instance priority] +instance (priority := 100) toExistsAddOfLE [NonUnitalSemiring R] [PartialOrder R] + [StarOrderedRing R] : ExistsAddOfLE R where + exists_add_of_le h := + match (le_iff _ _).mp h with + | ⟨p, _, hp⟩ => ⟨p, hp⟩ +#align star_ordered_ring.to_has_exists_add_of_le StarOrderedRing.toExistsAddOfLE + +-- see note [lower instance priority] +instance (priority := 100) toOrderedAddCommGroup [NonUnitalRing R] [PartialOrder R] + [StarOrderedRing R] : OrderedAddCommGroup R := + { show NonUnitalRing R by infer_instance, show PartialOrder R by infer_instance, + show StarOrderedRing R by infer_instance with } +#align star_ordered_ring.to_ordered_add_comm_group StarOrderedRing.toOrderedAddCommGroup + +-- set note [reducible non-instances] +/-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if +`y = x + star s * s` for some `s : R`. + +This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`) +and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances. + +If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see +`StarOrderedRing.ofNonnegIff` for a more convenient version. -/ +@[reducible] +def ofLeIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R] + (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y) + (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R := + { ‹StarRing R› with + add_le_add_left := @h_add + le_iff := fun x y => by + refine' ⟨fun h => _, _⟩ + · obtain ⟨p, hp⟩ := (h_le_iff x y).mp h + exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩ + · rintro ⟨p, hp, hpxy⟩ + revert x y hpxy + refine' AddSubmonoid.closure_induction hp _ (fun x y h => add_zero x ▸ h.ge) _ + · rintro _ ⟨s, rfl⟩ x y rfl + nth_rw 1 [← add_zero x] + refine' h_add _ x + exact (h_le_iff _ _).mpr ⟨s, by rw [zero_add]⟩ + · rintro a b ha hb x y rfl + nth_rw 1 [← add_zero x] + refine' h_add ((ha 0 _ (zero_add a).symm).trans (hb a _ rfl)) x } +#align star_ordered_ring.of_le_iff StarOrderedRing.ofLeIff + +-- set note [reducible non-instances] +/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to +show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated +by `star s * s` for `s : R`. -/ +@[reducible] +def ofNonnegIff [NonUnitalRing R] [PartialOrder R] [StarRing R] + (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y) + (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)) : + StarOrderedRing R := + { ‹StarRing R› with + add_le_add_left := @h_add + le_iff := fun x y => by + haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩ + simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x) } +#align star_ordered_ring.of_nonneg_iff StarOrderedRing.ofNonnegIff + +-- set note [reducible non-instances] +/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to +show that the nonnegative elements are precisely those elements of the form `star s * s` +for `s : R`. + +This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or +any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those +instances. -/ +@[reducible] +def ofNonnegIff' [NonUnitalRing R] [PartialOrder R] [StarRing R] + (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y) + (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) : StarOrderedRing R := + ofLeIff (@h_add) + (by + haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩ + simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)) +#align star_ordered_ring.of_nonneg_iff' StarOrderedRing.ofNonnegIff' + +theorem nonneg_iff [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] {x : R} : + 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s) := by + simp only [le_iff, zero_add, exists_eq_right'] +#align star_ordered_ring.nonneg_iff StarOrderedRing.nonneg_iff + +end StarOrderedRing + +section NonUnitalSemiring + +variable [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] + +theorem star_mul_self_nonneg (r : R) : 0 ≤ star r * r := + StarOrderedRing.nonneg_iff.mpr <| AddSubmonoid.subset_closure ⟨r, rfl⟩ +#align star_mul_self_nonneg star_mul_self_nonneg + +theorem star_mul_self_nonneg' (r : R) : 0 ≤ r * star r := by + simpa only [star_star] using star_mul_self_nonneg (star r) +#align star_mul_self_nonneg' star_mul_self_nonneg' + +theorem conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c := by + rw [StarOrderedRing.nonneg_iff] at ha + refine' AddSubmonoid.closure_induction ha (fun x hx => _) + (by rw [MulZeroClass.mul_zero, MulZeroClass.zero_mul]) fun x y hx hy => _ + · obtain ⟨x, rfl⟩ := hx + convert star_mul_self_nonneg (x * c) using 1 + rw [star_mul, ← mul_assoc, mul_assoc _ _ c] + · calc + 0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx + _ ≤ star c * x * c + star c * y * c := add_le_add_left hy _ + _ ≤ _ := by rw [mul_add, add_mul] +#align conjugate_nonneg conjugate_nonneg + +theorem conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c := by + simpa only [star_star] using conjugate_nonneg ha (star c) +#align conjugate_nonneg' conjugate_nonneg' + +theorem conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : + star c * a * c ≤ star c * b * c := by + rw [StarOrderedRing.le_iff] at hab ⊢ + obtain ⟨p, hp, rfl⟩ := hab + simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢ + exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩ +#align conjugate_le_conjugate conjugate_le_conjugate + +theorem conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c := + by simpa only [star_star] using conjugate_le_conjugate hab (star c) +#align conjugate_le_conjugate' conjugate_le_conjugate' + +end NonUnitalSemiring diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean index 2ea0bc1577a12..6c2bcd412514b 100644 --- a/Mathlib/Data/Complex/Basic.lean +++ b/Mathlib/Data/Complex/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kevin Buzzard, Mario Carneiro ! This file was ported from Lean 3 source module data.complex.basic -! leanprover-community/mathlib commit caa58cbf5bfb7f81ccbaca4e8b8ac4bc2b39cc1c +! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -1210,7 +1210,7 @@ scoped[ComplexOrder] attribute [instance] Complex.strictOrderedCommRing (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.) -/ protected def starOrderedRing : StarOrderedRing ℂ := -{ nonneg_iff := fun r => by + StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by refine' ⟨fun hr => ⟨Real.sqrt r.re, _⟩, fun h => _⟩ · have h₁ : 0 ≤ r.re := by rw [le_def] at hr @@ -1219,13 +1219,12 @@ protected def starOrderedRing : StarOrderedRing ℂ := rw [le_def] at hr exact hr.2.symm ext - · simp only [ofReal_im, star_def, ofReal_re, sub_zero, conj_re, mul_re, mul_zero, ← - Real.sqrt_mul h₁ r.re, Real.sqrt_mul_self h₁] + · simp only [ofReal_im, star_def, ofReal_re, sub_zero, conj_re, mul_re, mul_zero, + ← Real.sqrt_mul h₁ r.re, Real.sqrt_mul_self h₁] · simp only [h₂, add_zero, ofReal_im, star_def, zero_mul, conj_im, mul_im, mul_zero, neg_zero] · obtain ⟨s, rfl⟩ := h simp only [← normSq_eq_conj_mul_self, normSq_nonneg, zero_le_real, star_def] - add_le_add_left := by intros; simp [le_def] at *; assumption } #align complex.star_ordered_ring Complex.starOrderedRing scoped[ComplexOrder] attribute [instance] Complex.starOrderedRing diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean index fa5b856d3d5f9..cd87fa090d854 100644 --- a/Mathlib/Data/Real/Sqrt.lean +++ b/Mathlib/Data/Real/Sqrt.lean @@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Floris van Doorn, Yury Kudryashov ! This file was ported from Lean 3 source module data.real.sqrt -! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982 +! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ +import Mathlib.Algebra.Star.Order import Mathlib.Topology.Algebra.Order.MonotoneContinuity import Mathlib.Topology.Instances.NNReal import Mathlib.Tactic.Positivity @@ -467,11 +468,10 @@ theorem real_sqrt_le_nat_sqrt_succ {a : ℕ} : Real.sqrt ↑a ≤ Nat.sqrt a + 1 #align real.real_sqrt_le_nat_sqrt_succ Real.real_sqrt_le_nat_sqrt_succ instance : StarOrderedRing ℝ := - { Real.orderedAddCommGroup with - nonneg_iff := fun r => by - refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩ - rintro ⟨s, rfl⟩ - exact mul_self_nonneg s } + StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by + refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩ + rintro ⟨s, rfl⟩ + exact mul_self_nonneg s end Real diff --git a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean index fde57729c7fd9..0488ae2760ee0 100644 --- a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean +++ b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean @@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen ! This file was ported from Lean 3 source module linear_algebra.matrix.dot_product -! leanprover-community/mathlib commit 5ac1dab1670014b4c07a82c86a67f3d064a1b3e1 +! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ +import Mathlib.Algebra.Star.Order import Mathlib.Data.Matrix.Basic import Mathlib.LinearAlgebra.StdBasis diff --git a/docs/references.bib b/docs/references.bib index f4d9f6d40c71d..a100599230101 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1426,6 +1426,18 @@ @Book{ kechris1995 url = {https://doi.org/10.1007/978-1-4612-4190-4} } +@Article{ kelleyVaught1953, + author = {Kelley, J. L. and Vaught, R. L.}, + title = {The positive cone in {Banach} algebras}, + journal = {Trans. Am. Math. Soc.}, + issn = {0002-9947}, + volume = {74}, + pages = {44--55}, + year = {1953}, + language = {English}, + doi = {10.2307/1990847} +} + @Article{ kleiman1979, author = {Kleiman, Steven Lawrence}, title = {Misconceptions about {$K\_X$}},