Skip to content

Commit

Permalink
fix crash
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Jul 22, 2023
1 parent 3b1e3bc commit f92f012
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ instance : has_zero ((0 : quadratic_form R M₁) →qᵢ Q₂) :=
..(0 : M₁ →ₗ[R] M₂) } }

/-- There is a zero map from the trivial module. -/
instance [subsingleton M₁] : has_zero (Q₁ →qᵢ Q₂) :=
instance has_zero_of_subsingleton [subsingleton M₁] : has_zero (Q₁ →qᵢ Q₂) :=
{ zero :=
{ map_app' := λ m, subsingleton.elim 0 m ▸ (map_zero _).trans (map_zero _).symm,
..(0 : M₁ →ₗ[R] M₂) } }
Expand Down

0 comments on commit f92f012

Please sign in to comment.