Theorems · Inductive type · ring theory

StarRing

(R : Type u) → [NonUnitalNonAssocSemiring R] → Type u

A \-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation which is additive which makes `R` with its multiplicative structure into a \-multiplication (i.e. star (r * s) = star s * star r).

Defined in

Mathlib.Algebra.Star.Basic

Cited by

1,686 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiring