fix(ring_theory/subring): inclusion is a ring_hom! (#9849)

leanprover-community · Oct 21, 2021 · d8096aa · d8096aa
1 parent d8b0d1a
commit d8096aa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
@@ -833,7 +833,7 @@ namespace subring
 open ring_hom
 
 /-- The ring homomorphism associated to an inclusion of subrings. -/
-def inclusion {S T : subring R} (h : S ≤ T) : S →* T :=
+def inclusion {S T : subring R} (h : S ≤ T) : S →+* T :=
 S.subtype.cod_restrict' _ (λ x, h x.2)
 
 @[simp] lemma range_subtype (s : subring R) : s.subtype.range = s :=