@[class]
- to_is_add_subgroup : is_add_subgroup S
- to_is_submonoid : is_submonoid S
S is a subring: a set containing 1 and closed under multiplication, addition and and additive inverse.
@[instance]
Equations
- subset.ring = {add := add_comm_group.add subtype.add_comm_group, add_assoc := _, zero := add_comm_group.zero subtype.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg subtype.add_comm_group, add_left_neg := _, add_comm := _, mul := monoid.mul subtype.monoid, mul_assoc := _, one := monoid.one subtype.monoid, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[instance]
Equations
@[instance]
def
ring_hom.is_subring_preimage
{R : Type u}
{S : Type v}
[ring R]
[ring S]
(f : R →+* S)
(s : set S)
[is_subring s] :
is_subring (⇑f ⁻¹' s)
Equations
@[instance]
def
ring_hom.is_subring_image
{R : Type u}
{S : Type v}
[ring R]
[ring S]
(f : R →+* S)
(s : set R)
[is_subring s] :
is_subring (⇑f '' s)
Equations
@[instance]
def
ring_hom.is_subring_set_range
{R : Type u}
{S : Type v}
[ring R]
[ring S]
(f : R →+* S) :
is_subring (set.range ⇑f)
Equations
def
ring_hom.cod_restrict
{R : Type u}
{S : Type v}
[ring R]
[ring S]
(f : R →+* S)
(s : set S)
[is_subring s] :
Restrict the codomain of a ring homomorphism to a subring that includes the range.
Coersion S → R as a ring homormorphism
Equations
- is_subring.subtype S = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
is_subring.coe_subtype
{R : Type u}
[ring R]
{S : set R}
[is_subring S] :
⇑(is_subring.subtype S) = coe
@[instance]
Equations
- subset.comm_ring = {add := ring.add subset.ring, add_assoc := _, zero := ring.zero subset.ring, zero_add := _, add_zero := _, neg := ring.neg subset.ring, add_left_neg := _, add_comm := _, mul := ring.mul subset.ring, mul_assoc := _, one := ring.one subset.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Equations
@[instance]
Equations
- subring.domain S = {add := comm_ring.add subset.comm_ring, add_assoc := _, zero := comm_ring.zero subset.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg subset.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul subset.comm_ring, mul_assoc := _, one := comm_ring.one subset.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
@[instance]
def
is_subring.inter
{R : Type u}
[ring R]
(S₁ S₂ : set R)
[is_subring S₁]
[is_subring S₂] :
is_subring (S₁ ∩ S₂)
Equations
@[instance]
def
is_subring.Inter
{R : Type u}
[ring R]
{ι : Sort u_1}
(S : ι → set R)
[h : ∀ (y : ι), is_subring (S y)] :
is_subring (set.Inter S)
Equations
theorem
is_subring_Union_of_directed
{R : Type u}
[ring R]
{ι : Type u_1}
[hι : nonempty ι]
(s : ι → set R)
[∀ (i : ι), is_subring (s i)] :
(∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) → is_subring (⋃ (i : ι), s i)
Equations
theorem
ring.in_closure.rec_on
{R : Type u}
[ring R]
{s : set R}
{C : R → Prop}
{x : R} :
x ∈ ring.closure s → C 1 → C (-1) → (∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)) → (∀ {x y : R}, C x → C y → C (x + y)) → C x
@[instance]
Equations
theorem
ring.closure_subset
{R : Type u}
[ring R]
{s t : set R}
[is_subring t] :
s ⊆ t → ring.closure s ⊆ t
theorem
ring.closure_subset_iff
{R : Type u}
[ring R]
(s t : set R)
[is_subring t] :
ring.closure s ⊆ t ↔ s ⊆ t
theorem
ring.closure_mono
{R : Type u}
[ring R]
{s t : set R} :
s ⊆ t → ring.closure s ⊆ ring.closure t
theorem
ring.image_closure
{R : Type u}
[ring R]
{S : Type u_1}
[ring S]
(f : R →+* S)
(s : set R) :
⇑f '' ring.closure s = ring.closure (⇑f '' s)