Skip to content

Commit

Permalink
import
Browse files Browse the repository at this point in the history
  • Loading branch information
@fredrik-bakke
fredrik-bakke committed Oct 9, 2023
1 parent 55b4800 commit c398082
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ring-theory/division-rings.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module ring-theory.division-rings where
```agda
open import foundation.cartesian-product-types
open import foundation.identity-types
open import foundation.negation
open import foundation.negated-equality
open import foundation.universe-levels

open import ring-theory.invertible-elements-rings
Expand Down

0 comments on commit c398082

Please sign in to comment.