Theorems · Definition · ring theory

RingEquiv.toAddEquiv

{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 additive monoids underlying an equivalence of (semi)rings.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

13 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

MulMulAddAdd