Theorems · Inductive type · ring theory

RingEquiv

(R : Type u_7) → (S : Type u_8) → [Mul R] → [Mul S] → [Add R] → [Add S] → Type (max u_7 u_8)

An equivalence between two (non-unital non-associative semi)rings that preserves the algebraic structure.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

1,147 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

MulMulAddAdd