# 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

source
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

Instances

source
@[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

Instances For

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

Instances For