Meta properties of bijective ring homomorphisms

We show some meta properties of bijective ring homomorphisms.

Implementation details

We don't define a RingHom.Bijective predicate, but use fun f ↦ Function.Bijective f as the ring hom property.

theorem RingHom.Bijective.containsIdentities : ContainsIdentities fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f

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

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

theorem RingHom.Bijective.isStableUnderBaseChange : IsStableUnderBaseChange fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f

theorem RingHom.Bijective.ofLocalizationSpan : OfLocalizationSpan fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f