# 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/QuotientGroup.lean`

- quotient module:
`Mathlib/LinearAlgebra/Quotient.lean`

- quotient ring:
`Mathlib/RingTheory/Ideal/Quotient.lean`

## Notations #

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

`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

## Instances

`HasQuotient.Quotient A b`

(with notation `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

## Instances For

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))