English
There is a natural bijection between ring-language isomorphisms and ring isomorphisms: (Language.ring.Equiv R S) ≃ (R ≃+* S).
Русский
Существует естественная взаимно однозначная корреляция между эквивалентностями по языку колец и кольцевыми изоморфизмами: (Language.ring.Equiv R S) эквивалентно (R ≃+* S).
LaTeX
$$$ (\\text{Language.ring.Equiv } R S) \\simeq (R \\cong+* S) $$$
Lean4
/-- An isomorphism in the language of rings is a ring isomorphism -/
def languageEquivEquivRingEquiv {R S : Type*} [NonAssocRing R] [NonAssocRing S] [CompatibleRing R] [CompatibleRing S] :
(Language.ring.Equiv R S) ≃ (R ≃+* S) :=
{ toFun
f :=
{
f with
map_add' := by
intro x y
simpa using f.map_fun addFunc ![x, y]
map_mul' := by
intro x y
simpa using f.map_fun mulFunc ![x, y] }
invFun
f :=
{ f with
map_fun' := fun {n} f => by cases f <;> simp
map_rel' := fun {n} f => by cases f } }
