Meta properties of injective ring homomorphisms

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

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