Theorems · Definition · group theory

Ring.inverse

{M₀ : Type u_2} → [MonoidWithZero M₀] → M₀ → M₀

Introduce a function inverse on a monoid with zero M₀, which sends x to x⁻¹ if x is invertible and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus. Note that while this is in the Ring namespace for brevity, it requires the weaker assumption MonoidWithZero M₀ instead of Ring M₀.

Defined in

Mathlib.Algebra.GroupWithZero.Units.Basic

Cited by

160 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 92 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MonoidWithZero