File tree Expand file tree Collapse file tree
Mathlib/Analysis/CStarAlgebra Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -344,7 +344,6 @@ instance instNonUnitalSemiring [Fintype n] [NonUnitalSemiring A] :
344344 NonUnitalSemiring (CStarMatrix n n A) :=
345345 inferInstanceAs <| NonUnitalSemiring (Matrix n n A)
346346
347- set_option backward.inferInstanceAs.wrap false in
348347instance instNonAssocSemiring [Fintype n] [DecidableEq n] [NonAssocSemiring A] :
349348 NonAssocSemiring (CStarMatrix n n A) :=
350349 inferInstanceAs <| NonAssocSemiring (Matrix n n A)
@@ -353,17 +352,14 @@ instance instNonUnitalRing [Fintype n] [NonUnitalRing A] :
353352 NonUnitalRing (CStarMatrix n n A) :=
354353 inferInstanceAs <| NonUnitalRing (Matrix n n A)
355354
356- set_option backward.inferInstanceAs.wrap false in
357355instance instNonAssocRing [Fintype n] [DecidableEq n] [NonAssocRing A] :
358356 NonAssocRing (CStarMatrix n n A) :=
359357 inferInstanceAs <| NonAssocRing (Matrix n n A)
360358
361- set_option backward.inferInstanceAs.wrap false in
362359instance instSemiring [Fintype n] [DecidableEq n] [Semiring A] :
363360 Semiring (CStarMatrix n n A) :=
364361 inferInstanceAs <| Semiring (Matrix n n A)
365362
366- set_option backward.inferInstanceAs.wrap false in
367363instance instRing [Fintype n] [DecidableEq n] [Ring A] : Ring (CStarMatrix n n A) :=
368364 inferInstanceAs <| Ring (Matrix n n A)
369365
You can’t perform that action at this time.
0 commit comments