Documentation

Mathlib.RingTheory.Ideal.Defs

Ideals over a ring #

This file defines Ideal R, the type of (left) ideals over a ring R. Note that over commutative rings, left ideals and two-sided ideals are equivalent.

Implementation notes #

Ideal R is implemented using Submodule R R, where • is interpreted as *.

TODO #

Support right ideals, and two-sided ideals over non-commutative rings.

source
@[reducible, inline]
abbrev Ideal (R : Type u) [Semiring R] :
Type u

A (left) ideal in a semiring R is an additive submonoid s such that a * b ∈ s whenever b ∈ s. If R is a ring, then s is an additive subgroup.

Equations
Instances For
    source
    theorem Ideal.zero_mem {α : Type u} [Semiring α] (I : Ideal α) :
    0 ∈ I
    source
    theorem Ideal.add_mem {α : Type u} [Semiring α] (I : Ideal α) {a b : α} :
    a ∈ I → b ∈ I → a + b ∈ I
    source
    theorem Ideal.mul_mem_left {α : Type u} [Semiring α] (I : Ideal α) (a : α) {b : α} :
    b ∈ I → a * b ∈ I
    source
    theorem Ideal.ext {α : Type u} [Semiring α] {I J : Ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) :
    I = J
    source
    @[simp]
    theorem Ideal.unit_mul_mem_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x y : α} (hy : IsUnit y) :
    y * x ∈ I ↔ x ∈ I
    source
    @[simp]
    theorem Ideal.mul_unit_mem_iff_mem {α : Type u} [CommSemiring α] (I : Ideal α) {x y : α} (hy : IsUnit y) :
    x * y ∈ I ↔ x ∈ I
    source
    theorem Ideal.mul_mem_right {α : Type u} {a : α} (b : α) [CommSemiring α] (I : Ideal α) (h : a ∈ I) :
    a * b ∈ I
    source
    theorem Ideal.mem_of_dvd {α : Type u} {a b : α} [CommSemiring α] (I : Ideal α) (hab : a ∣ b) (ha : a ∈ I) :
    b ∈ I
    source
    theorem Ideal.pow_mem_of_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) (ha : a ∈ I) (n : ℕ) (hn : 0 < n) :
    a ^ n ∈ I
    source
    theorem Ideal.pow_mem_of_pow_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) {m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) :
    a ^ n ∈ I
    source
    theorem Ideal.neg_mem_iff {α : Type u} [Ring α] (I : Ideal α) {a : α} :
    -a ∈ I ↔ a ∈ I
    source
    theorem Ideal.add_mem_iff_left {α : Type u} [Ring α] (I : Ideal α) {a b : α} :
    b ∈ I → (a + b ∈ I ↔ a ∈ I)
    source
    theorem Ideal.add_mem_iff_right {α : Type u} [Ring α] (I : Ideal α) {a b : α} :
    a ∈ I → (a + b ∈ I ↔ b ∈ I)
    source
    theorem Ideal.sub_mem {α : Type u} [Ring α] (I : Ideal α) {a b : α} :
    a ∈ I → b ∈ I → a - b ∈ I
    source
    theorem Ideal.mul_sub_mul_mem {R : Type u_1} [CommRing R] (I : Ideal R) {a b c d : R} (h1 : a - b ∈ I) (h2 : c - d ∈ I) :
    a * c - b * d ∈ I