## Stream: maths

### Topic: Bijective Ring Homorphism an Isomorphism

#### Jordan Brown (Jul 29 2020 at 22:50):

Does mathlib have the theorem showing that a bijective ring homomorphism is an isomorphism? It seems to be missing from the data.equiv.ring, is there somewhere else I should look?

#### Matt Earnshaw (Jul 29 2020 at 23:59):

import algebra.category.CommRing.basic
#check ring_equiv.to_Ring_iso


#### Thomas Browning (Jul 30 2020 at 00:05):

But there you're already assuming that you have a ring equivalence (rather than a bijective ring homomorphism)

oops

#### Adam Topaz (Jul 30 2020 at 00:46):

You can combine src#equiv.of_bijective to get this easily.

#### Adam Topaz (Jul 30 2020 at 00:51):

import data.equiv.basic
import data.equiv.ring

variables {A : Type*} [ring A]
variables {B : Type*} [ring B]

noncomputable def ring_equiv_of_bij_hom (f : A →+* B) (h : function.bijective f) : A ≃+* B :=
{ map_mul' := by apply ring_hom.map_mul,
..show A ≃ B, by exact equiv.of_bijective _ h }


There might be a better way. Or mathlib might already have something like this.

#### Johan Commelin (Jul 30 2020 at 03:55):

Can't you golf that to

noncomputable def ring_equiv_of_bij_hom (f : A →+* B) (h : function.bijective f) : A ≃+* B :=
{ .. f, .. equiv.of_bijective _ h }


Last updated: May 19 2021 at 00:40 UTC