Skip to content

Commit

Permalink
remove assumption
Browse files Browse the repository at this point in the history
  • Loading branch information
zjj committed Aug 15, 2024
1 parent 5eab163 commit d8ab250
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion BrauerGroup/Profinite/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ def ofFiniteGrp (G : FiniteGrp) : ProfiniteGrp :=

section

variable {J : Type v} [Category J] [IsFiltered J] (F : J ⥤ FiniteGrp)
variable {J : Type v} [Category J] (F : J ⥤ FiniteGrp)

attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeToSort

Expand Down

0 comments on commit d8ab250

Please sign in to comment.