Ideal quotients #
This file defines ideal quotients as a special case of submodule quotients and proves some basic results about these quotients.
See Algebra.RingQuot
for quotients of semirings.
Main definitions #
Equations
- Ideal.Quotient.instUniqueQuotientTop = { default := 0, uniq := ⋯ }
The quotient by a maximal ideal is a group with zero. This is a def
rather than instance
,
since users will have computable inverses in some applications.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient by a two-sided ideal that is maximal as a left ideal is a division ring.
This is a def
rather than instance
, since users
will have computable inverses (and qsmul
, ratCast
) in some applications.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient of a commutative ring by a maximal ideal is a field.
This is a def
rather than instance
, since users
will have computable inverses (and qsmul
, ratCast
) in some applications.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Instances For
A ring is made up of a disjoint union of cosets of an ideal.