Algebraic quotients #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
has_quotientinstance. 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
has_quotient 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.
Instances of this typeclass
Instances of other typeclasses for
has_quotient.quotient A b (with notation
A ⧸ b) is the quotient of the type
This differs from
has_quotient.quotient' in that the
A argument is explicit, which is necessary
to make Lean show the notation in the goal state.