Skip to content

Commit

Permalink
chore(linear_algebra/matrix/dot_product): weaken typeclasses (#18798)
Browse files Browse the repository at this point in the history
This makes unification slightly harder on Lean, so `: _`s are added.

Fixes a stupid error in #18783
  • Loading branch information
eric-wieser committed Apr 12, 2023
1 parent 347636a commit 5ac1dab
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/linear_algebra/matrix/dot_product.lean
Expand Up @@ -79,16 +79,16 @@ variables [fintype n]

/-- Note that this applies to `ℂ` via `complex.strict_ordered_comm_ring`. -/
@[simp] lemma dot_product_star_self_eq_zero
[strict_ordered_ring R] [star_ordered_ring R] [no_zero_divisors R] {v : n → R} :
[partial_order R] [non_unital_ring R] [star_ordered_ring R] [no_zero_divisors R] {v : n → R} :
dot_product (star v) v = 0 ↔ v = 0 :=
(finset.sum_eq_zero_iff_of_nonneg $ λ i _, @star_mul_self_nonneg _ _ _ _ (v i)).trans $
(finset.sum_eq_zero_iff_of_nonneg $ λ i _, (@star_mul_self_nonneg _ _ _ _ (v i) : _)).trans $
by simp [function.funext_iff, mul_eq_zero]

/-- Note that this applies to `ℂ` via `complex.strict_ordered_comm_ring`. -/
@[simp] lemma dot_product_self_star_eq_zero
[strict_ordered_ring R] [star_ordered_ring R] [no_zero_divisors R] {v : n → R} :
[partial_order R] [non_unital_ring R] [star_ordered_ring R] [no_zero_divisors R] {v : n → R} :
dot_product v (star v) = 0 ↔ v = 0 :=
(finset.sum_eq_zero_iff_of_nonneg $ λ i _, @star_mul_self_nonneg' _ _ _ _ (v i)).trans $
(finset.sum_eq_zero_iff_of_nonneg $ λ i _, (@star_mul_self_nonneg' _ _ _ _ (v i) : _)).trans $
by simp [function.funext_iff, mul_eq_zero]

end self
Expand Down

0 comments on commit 5ac1dab

Please sign in to comment.