Semirings and rings #
This file gives lemmas about semirings, rings and domains.
This is analogous to Algebra.Group.Basic
,
the difference being that the former is about +
and *
separately, while
the present file is about their interaction.
For the definitions of semirings and rings see Algebra.Ring.Defs
.
Additive homomorphisms preserve bit0
.
Left multiplication by an element of a (semi)ring is an AddMonoidHom
Instances For
Right multiplication by an element of a (semi)ring is an AddMonoidHom
Instances For
Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with
its roots. This particular version states that if we have a root x
of a monic quadratic
polynomial, then there is another root y
such that x + y
is negative the a_1
coefficient
and x * y
is the a_0
coefficient.