Theorems · Inductive type · group theory

MulDivCancelClass

(M₀ : Type u_2) → [MonoidWithZero M₀] → [Div M₀] → Prop

Prop-valued mixin for a monoid with zero to be equipped with a cancelling division. The obvious use case is groups with zero, but this condition is also satisfied by ℕ, ℤ and, more generally, any Euclidean domain.

Defined in

Mathlib.Algebra.GroupWithZero.Defs

Cited by

5 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

MonoidWithZeroDiv