Algebraic quotients

This file defines notation for algebraic quotients, e.g. quotient groups G ⧸ H, quotient modules M ⧸ N and ideal quotients R ⧸ I.

The actual quotient structures are defined in the following files:

• Quotient Group: Mathlib/GroupTheory/Cosets/Defs.lean
• Quotient Module: Mathlib/LinearAlgebra/Quotient/Defs.lean
• Quotient Ring: Mathlib/RingTheory/Ideal/Quotient/Defs.lean

Notation

The following notation is introduced:

• G ⧸ H stands for the quotient of the type G by some term H (for example, H can be a normal subgroup of G). To implement this notation for other quotients, you should provide a HasQuotient instance. Note that since G can usually be inferred from H, _ ⧸ H can also be used, but this is less readable.

Tags

quotient, group quotient, quotient group, module quotient, quotient module, ring quotient, ideal quotient, quotient ring

class HasQuotient (A : outParam (Type u)) (B : Type v) : Type (max (u + 1) (v + 1))

HasQuotient A B is a notation typeclass that allows us to write A ⧸ b for b : B. This allows the usual notation for quotients of algebraic structures, such as groups, modules and rings.

A is a parameter, despite being unused in the definition below, so it appears in the notation.

• quotient' : B → Type (max u v)

  auxiliary quotient function, the one used will have A explicit

@[reducible, inline]

abbrev HasQuotient.Quotient (A : outParam (Type u)) {B : Type v} [HasQuotient A B] (b : B) : Type (max u v)

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

This differs from HasQuotient.quotient' in that the A argument is explicit, which is necessary to make Lean show the notation in the goal state.

Equations

• (A ⧸ b) = HasQuotient.quotient' b

def «term_⧸_» : Lean.TrailingParserDescr

Quotient notation based on the HasQuotient typeclass

Equations

• «term_⧸_» = Lean.ParserDescr.trailingNode `«term_⧸_» 35 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⧸ ") (Lean.ParserDescr.cat `term 34))