Algebraic quotients #
This file defines notation for algebraic quotients, e.g. quotient groups
G ⧸ H,
M ⧸ N and ideal quotients
R ⧸ I.
The actual quotient structures are defined in the following files:
- quotient group:
- quotient module:
- quotient ring:
The following notation is introduced:
G ⧸ Hstands for the quotient of the type
Gby some term
Hcan be a normal subgroup of
G). To implement this notation for other quotients, you should provide a
HasQuotientinstance. Note that since
Gcan usually be inferred from
_ ⧸ Hcan also be used, but this is less readable.
quotient, group quotient, quotient group, module quotient, quotient module, ring quotient, ideal quotient, quotient ring
auxiliary quotient function, the one used will have
Aexplicitquotient' : B → Type (maxuv)
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.
HasQuotient.Quotient A b (with notation
A ⧸ b) is the quotient
of the type
This differs from
HasQuotient.quotient' in that the
A argument is
explicit, which is necessary to make Lean show the notation in the
- (A ⧸ b) = HasQuotient.quotient' b
Quotient notation based on the
- «term_⧸_» = Lean.ParserDescr.trailingNode `term_⧸_ 35 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⧸ ") (Lean.ParserDescr.cat `term 34))