Theorems · Definition · ring theory

RingEquiv.symm

{R : Type u_4} →
  {S : Type u_5} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → R ≃+* S → S ≃+* R

The inverse of a ring isomorphism is a ring isomorphism.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

567 results in Mathlib

Foundations

Depth 16 from the axioms, rests on 93 definitions · uses Quot.sound

Assumes

MulMulAddAdd