Skip to content

Commit

Permalink
chore(ring_theory/prod): move file to algebra/ring/prod (#3540)
Browse files Browse the repository at this point in the history
  • Loading branch information
ChrisHughes24 committed Jul 24, 2020
1 parent 47efcf3 commit 4d81149
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 1 deletion.
File renamed without changes.
2 changes: 1 addition & 1 deletion src/ring_theory/subsemiring.lean
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/

import ring_theory.prod
import algebra.ring.prod
import group_theory.submonoid
import data.equiv.ring

Expand Down

0 comments on commit 4d81149

Please sign in to comment.