fix(ring_theory/subsemiring/basic): make inclusion a ring_hom, no…

…t a `monoid_hom` (#13746)
leanprover-community · Apr 27, 2022 · e89510c · e89510c
1 parent 60bb071
commit e89510c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean
@@ -873,7 +873,7 @@ namespace subsemiring
 open ring_hom
 
 /-- The ring homomorphism associated to an inclusion of subsemirings. -/
-def inclusion {S T : subsemiring R} (h : S ≤ T) : S →* T :=
+def inclusion {S T : subsemiring R} (h : S ≤ T) : S →+* T :=
 S.subtype.cod_srestrict _ (λ x, h x.2)
 
 @[simp] lemma srange_subtype (s : subsemiring R) : s.subtype.srange = s :=