Theorems · Definition · ring theory

RingEquiv.toMulEquiv

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

The equivalence of multiplicative monoids underlying an equivalence of (semi)rings.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

26 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

MulMulAddAdd