Theorems · Definition

HasQuotient.Quotient

(A : outParam (Type u)) → {B : Type v} → [self : HasQuotient A B] → B → Type (max u v)

HasQuotient.Quotient A b (denoted as A ⧸ b) is the quotient of the type A by b.

Defined in

Mathlib.Algebra.Quotient

Cited by

2,301 results in Mathlib

Foundations

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

Assumes

HasQuotient