Theorems · Definition · functional analysis

IsQuasiregular

{R : Type u_1} → [NonUnitalSemiring R] → R → Prop

In a non-unital semiring R, an element x : R satisfies IsQuasiregular if it is a unit under the monoid operation fun x y ↦ y + x + x * y.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

18 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalSemiring