feat: port algebra.hom.centroid (#1325)

Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr> Co-authored-by: maxwell-thum <119913396+maxwell-thum@users.noreply.github.com>
leanprover-community · Jan 17, 2023 · 631abde · 631abde
1 parent 98d34d7
commit 631abde
Show file tree

Hide file tree

Showing 2 changed files with 528 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -55,6 +55,7 @@ import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.HierarchyDesign
 import Mathlib.Algebra.Hom.Aut
+import Mathlib.Algebra.Hom.Centroid
 import Mathlib.Algebra.Hom.Commute
 import Mathlib.Algebra.Hom.Embedding
 import Mathlib.Algebra.Hom.Equiv.Basic