Meta properties of injective ring homomorphisms

theorem RingHom.injective_stableUnderComposition : RingHom.StableUnderComposition fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Injective ⇑f

theorem RingHom.injective_respectsIso : RingHom.RespectsIso fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Injective ⇑f