Ideals generated by a set of elements #
This file defines Ideal.span s
as the ideal generated by the subset s
of the ring.
TODO #
Support right ideals, and two-sided ideals over non-commutative rings.
A ring is a principal ideal ring if all (left) ideals are principal.
- principal (S : Ideal R) : Submodule.IsPrincipal S
Instances
The ideal generated by a subset of a ring
Instances For
@[simp]
The ideal generated by an arbitrary binary relation.
Equations
- Ideal.ofRel r = Submodule.span α {x : α | ∃ (a : α) (b : α), r a b ∧ x + b = a}
Instances For
theorem
Ideal.span_singleton_mul_right_unit
{α : Type u}
[CommSemiring α]
{a : α}
(h2 : IsUnit a)
(x : α)
: