Documentation

Mathlib.Algebra.Ring.Basic

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.

@[simp]
theorem AddHom.mulLeft_apply {R : Type u_1} [Distrib R] (r : R) :
(AddHom.mulLeft r) = fun (x : R) => r * x
def AddHom.mulLeft {R : Type u_1} [Distrib R] (r : R) :
AddHom R R

Left multiplication by an element of a type with distributive multiplication is an AddHom.

Equations
Instances For
    @[simp]
    theorem AddHom.mulRight_apply {R : Type u_1} [Distrib R] (r : R) :
    (AddHom.mulRight r) = fun (a : R) => a * r
    def AddHom.mulRight {R : Type u_1} [Distrib R] (r : R) :
    AddHom R R

    Left multiplication by an element of a type with distributive multiplication is an AddHom.

    Equations
    Instances For
      @[simp, deprecated]
      theorem map_bit0 {α : Type u_2} {β : Type u_3} {F : Type u_4} [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : α) :
      f (bit0 a) = bit0 (f a)

      Additive homomorphisms preserve bit0.

      Left multiplication by an element of a (semi)ring is an AddMonoidHom

      Equations
      • AddMonoidHom.mulLeft r = { toZeroHom := { toFun := fun (x : R) => r * x, map_zero' := }, map_add' := }
      Instances For

        Right multiplication by an element of a (semi)ring is an AddMonoidHom

        Equations
        Instances For
          @[simp]
          theorem AddMonoidHom.coe_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) :
          (AddMonoidHom.mulRight r) = fun (x : R) => x * r
          instance hasDistribNeg {α : Type u_2} [Mul α] [HasDistribNeg α] :
          Equations
          @[simp]
          theorem inv_neg' {α : Type u_2} [Group α] [HasDistribNeg α] (a : α) :
          theorem vieta_formula_quadratic {α : Type u_2} [NonUnitalCommRing α] {b : α} {c : α} {x : α} (h : x * x - b * x + c = 0) :
          ∃ (y : α), y * y - b * y + c = 0 x + y = b x * y = c

          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.

          theorem succ_ne_self {α : Type u_2} [NonAssocRing α] [Nontrivial α] (a : α) :
          a + 1 a
          theorem pred_ne_self {α : Type u_2} [NonAssocRing α] [Nontrivial α] (a : α) :
          a - 1 a
          Equations
          • =
          instance IsDomain.to_noZeroDivisors (α : Type u_2) [Ring α] [IsDomain α] :
          Equations
          • =
          Equations
          • =
          Equations
          • =