doc-next-gen

Mathlib.RingTheory.NonUnitalSubring.Defs

Module docstring

{"# NonUnitalSubrings

Let R be a non-unital ring. This file defines the \"bundled\" non-unital subring type NonUnitalSubring R, a type whose terms correspond to non-unital subrings of R. This is the preferred way to talk about non-unital subrings in mathlib.

Main definitions

Notation used here:

(R : Type u) [NonUnitalRing R] (S : Type u) [NonUnitalRing S] (f g : R →ₙ+* S) (A : NonUnitalSubring R) (B : NonUnitalSubring S) (s : Set R)

  • NonUnitalSubring R : the type of non-unital subrings of a ring R.

Implementation notes

A non-unital subring is implemented as a NonUnitalSubsemiring which is also an additive subgroup.

Lattice inclusion (e.g. ≤ and ⊓) is used rather than set notation (⊆ and ∩), although ∈ is defined as membership of a non-unital subring's underlying set.

Tags

non-unital subring ","## Partial order "}

NonUnitalSubringClass structure
(S : Type*) (R : Type u) [NonUnitalNonAssocRing R] [SetLike S R] : Prop extends NonUnitalSubsemiringClass S R, NegMemClass S R
Full source 
/-- `NonUnitalSubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
are both a multiplicative submonoid and an additive subgroup. -/
class NonUnitalSubringClass (S : Type*) (R : Type u) [NonUnitalNonAssocRing R] [SetLike S R] : Prop
  extends NonUnitalSubsemiringClass S R, NegMemClass S R where
Non-unital subring class
Informal description
The structure `NonUnitalSubringClass S R` asserts that `S` is a type of subsets of a non-unital non-associative ring `R` that are both closed under multiplication (forming a multiplicative submonoid) and closed under addition and negation (forming an additive subgroup). In other words, a subset `s ⊆ R` in `S` satisfies: 1. Closure under multiplication: for any $x, y \in s$, $x * y \in s$ 2. Closure under addition: for any $x, y \in s$, $x + y \in s$ 3. Closure under negation: for any $x \in s$, $-x \in s$ This structure extends both `NonUnitalSubsemiringClass` (which provides the multiplicative and additive closure) and `NegMemClass` (which provides the negation closure).
NonUnitalSubringClass.addSubgroupClass instance
(S : Type*) (R : Type u) [SetLike S R] [NonUnitalNonAssocRing R] [h : NonUnitalSubringClass S R] : AddSubgroupClass S R
Full source 
instance (priority := 100) NonUnitalSubringClass.addSubgroupClass (S : Type*) (R : Type u)
    [SetLike S R] [NonUnitalNonAssocRing R] [h : NonUnitalSubringClass S R] :
    AddSubgroupClass S R :=
  { h with }
Non-unital Subrings are Additive Subgroups
Informal description
For any type `S` representing subsets of a non-unital non-associative ring `R`, if `S` has a `NonUnitalSubringClass` instance, then `S` also has an `AddSubgroupClass` instance. This means that any subset `s ⊆ R` in `S` is closed under addition and negation, forming an additive subgroup of `R`.
NonUnitalSubringClass.toNonUnitalNonAssocRing instance
: NonUnitalNonAssocRing s
Full source 
/-- A non-unital subring of a non-unital ring inherits a non-unital ring structure -/
instance (priority := 75) toNonUnitalNonAssocRing : NonUnitalNonAssocRing s := fast_instance%
  Subtype.val_injective.nonUnitalNonAssocRing _ rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Non-unital Subrings Inherit Non-unital Non-associative Ring Structure
Informal description
For any subset $s$ of a non-unital non-associative ring $R$ that forms a non-unital subring, $s$ inherits a non-unital non-associative ring structure from $R$.
NonUnitalSubringClass.toNonUnitalRing instance
{R : Type*} [NonUnitalRing R] [SetLike S R] [NonUnitalSubringClass S R] (s : S) : NonUnitalRing s
Full source 
/-- A non-unital subring of a non-unital ring inherits a non-unital ring structure -/
instance (priority := 75) toNonUnitalRing {R : Type*} [NonUnitalRing R] [SetLike S R]
    [NonUnitalSubringClass S R] (s : S) : NonUnitalRing s := fast_instance%
  Subtype.val_injective.nonUnitalRing _ rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Non-unital Subrings Inherit Non-unital Ring Structure
Informal description
For any subset $s$ of a non-unital ring $R$ that forms a non-unital subring, $s$ inherits a non-unital ring structure from $R$.
NonUnitalSubringClass.toNonUnitalCommRing instance
{R} [NonUnitalCommRing R] [SetLike S R] [NonUnitalSubringClass S R] : NonUnitalCommRing s
Full source 
/-- A non-unital subring of a `NonUnitalCommRing` is a `NonUnitalCommRing`. -/
instance (priority := 75) toNonUnitalCommRing {R} [NonUnitalCommRing R] [SetLike S R]
    [NonUnitalSubringClass S R] : NonUnitalCommRing s := fast_instance%
  Subtype.val_injective.nonUnitalCommRing _ rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Non-unital Subrings Inherit Non-unital Commutative Ring Structure
Informal description
For any non-unital commutative ring $R$ and a subset $s$ of $R$ that forms a non-unital subring, $s$ inherits a non-unital commutative ring structure from $R$.
NonUnitalSubringClass.subtype definition
(s : S) : s →ₙ+* R
Full source 
/-- The natural non-unital ring hom from a non-unital subring of a non-unital ring `R` to `R`. -/
def subtype (s : S) : s →ₙ+* R :=
  { NonUnitalSubsemiringClass.subtype s,
    AddSubgroupClass.subtype s with
    toFun := Subtype.val }
Inclusion homomorphism of a non-unital subring
Informal description
The canonical non-unital ring homomorphism from a non-unital subring $s$ of a non-unital ring $R$ to $R$, mapping each element of $s$ to itself in $R$.
NonUnitalSubringClass.subtype_apply theorem
(x : s) : subtype s x = x
Full source 
@[simp]
theorem subtype_apply (x : s) : subtype s x = x :=
  rfl
Inclusion Homomorphism Acts as Identity on Non-Unital Subring Elements
Informal description
For any element $x$ in a non-unital subring $s$ of a non-unital ring $R$, the inclusion homomorphism $\text{subtype}\, s$ maps $x$ to itself in $R$, i.e., $\text{subtype}\, s (x) = x$.
NonUnitalSubringClass.subtype_injective theorem
: Function.Injective (subtype s)
Full source 
theorem subtype_injective : Function.Injective (subtype s) :=
  Subtype.coe_injective
Injectivity of Non-unital Subring Inclusion Homomorphism
Informal description
The canonical inclusion homomorphism from a non-unital subring $s$ of a non-unital ring $R$ to $R$ is injective. In other words, if two elements of $s$ are mapped to the same element in $R$ under this homomorphism, then they must be equal in $s$.
NonUnitalSubringClass.coe_subtype theorem
: (subtype s : s → R) = Subtype.val
Full source 
@[simp]
theorem coe_subtype : (subtype s : s → R) = Subtype.val :=
  rfl
Inclusion Homomorphism Equals Subtype Projection for Non-unital Subrings
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, the inclusion homomorphism from $s$ to $R$ is equal to the canonical projection map $\text{Subtype.val} : s \to R$ that sends each element of $s$ to itself in $R$.
NonUnitalSubring structure
(R : Type u) [NonUnitalNonAssocRing R] extends NonUnitalSubsemiring R, AddSubgroup R
Full source 
/-- `NonUnitalSubring R` is the type of non-unital subrings of `R`. A non-unital subring of `R`
is a subset `s` that is a multiplicative subsemigroup and an additive subgroup. Note in particular
that it shares the same 0 as R. -/
structure NonUnitalSubring (R : Type u) [NonUnitalNonAssocRing R] extends
  NonUnitalSubsemiring R, AddSubgroup R
Non-unital subring
Informal description
A non-unital subring of a non-unital non-associative ring $R$ is a subset $s$ of $R$ that is closed under addition, negation, and multiplication, and contains the zero element. It inherits the additive and multiplicative structures from $R$.
NonUnitalSubring.toSubsemigroup definition
(s : NonUnitalSubring R) : Subsemigroup R
Full source 
/-- The underlying submonoid of a `NonUnitalSubring`. -/
def toSubsemigroup (s : NonUnitalSubring R) : Subsemigroup R :=
  { s.toNonUnitalSubsemiring.toSubsemigroup with carrier := s.carrier }
Underlying multiplicative subsemigroup of a non-unital subring
Informal description
Given a non-unital subring $s$ of a non-unital non-associative ring $R$, the function returns the underlying multiplicative subsemigroup of $s$, which is a subset of $R$ closed under multiplication.
NonUnitalSubring.instSetLike instance
: SetLike (NonUnitalSubring R) R
Full source 
instance : SetLike (NonUnitalSubring R) R where
  coe s := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective h
Set-like Structure of Non-unital Subrings
Informal description
For any non-unital non-associative ring $R$, the type of non-unital subrings of $R$ forms a set-like structure, where each non-unital subring can be viewed as a subset of $R$ with the inherited operations.
NonUnitalSubring.ofClass definition
{S R : Type*} [NonUnitalNonAssocRing R] [SetLike S R] [NonUnitalSubringClass S R] (s : S) : NonUnitalSubring R
Full source 
/-- The actual `NonUnitalSubring` obtained from an element of a `NonUnitalSubringClass`. -/
@[simps]
def ofClass {S R : Type*} [NonUnitalNonAssocRing R] [SetLike S R] [NonUnitalSubringClass S R]
    (s : S) : NonUnitalSubring R where
  carrier := s
  add_mem' := add_mem
  zero_mem' := zero_mem _
  mul_mem' := mul_mem
  neg_mem' := neg_mem
Construction of a non-unital subring from a subset with closure properties
Informal description
Given a type `S` with a set-like structure on a non-unital non-associative ring `R`, and an instance of `NonUnitalSubringClass S R`, the function `NonUnitalSubring.ofClass` constructs a `NonUnitalSubring R` from an element `s : S`. The underlying set of this subring is `s`, and it inherits the additive and multiplicative closure properties from `s`. More precisely, for any subset `s` of `R` that is closed under addition, multiplication, negation, and contains zero, `NonUnitalSubring.ofClass s` returns the corresponding bundled non-unital subring structure.
NonUnitalSubring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg instance
: CanLift (Set R) (NonUnitalSubring R) (↑) (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → -x ∈ s)
Full source 
instance (priority := 100) : CanLift (Set R) (NonUnitalSubring R) (↑)
    (fun s ↦ 0 ∈ s0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧
      (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → -x ∈ s) where
  prf s h :=
    ⟨ { carrier := s
        zero_mem' := h.1
        add_mem' := h.2.1
        mul_mem' := h.2.2.1
        neg_mem' := h.2.2.2 },
      rfl ⟩
Lifting Condition for Non-unital Subrings
Informal description
For any non-unital non-associative ring $R$, a subset $s$ of $R$ can be lifted to a non-unital subring if and only if $s$ contains $0$ and is closed under addition, multiplication, and negation. Specifically, the lifting condition requires that $0 \in s$, and for all $x, y \in s$, both $x + y \in s$ and $x * y \in s$, and for all $x \in s$, $-x \in s$.
NonUnitalSubring.instNonUnitalSubringClass instance
: NonUnitalSubringClass (NonUnitalSubring R) R
Full source 
instance : NonUnitalSubringClass (NonUnitalSubring R) R where
  zero_mem s := s.zero_mem'
  add_mem {s} := s.add_mem'
  mul_mem {s} := s.mul_mem'
  neg_mem {s} := s.neg_mem'
Non-unital Subrings Form a NonUnitalSubringClass
Informal description
The type of non-unital subrings of a non-unital non-associative ring $R$ forms a `NonUnitalSubringClass`, meaning it satisfies the closure properties under addition, multiplication, and negation.
NonUnitalSubring.mem_carrier theorem
{s : NonUnitalSubring R} {x : R} : x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s
Full source 
theorem mem_carrier {s : NonUnitalSubring R} {x : R} : x ∈ s.toNonUnitalSubsemiringx ∈ s.toNonUnitalSubsemiring ↔ x ∈ s :=
  Iff.rfl
Membership Criterion for Non-unital Subrings via Underlying Subsemiring
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$ and any element $x \in R$, the element $x$ belongs to the underlying non-unital subsemiring of $s$ if and only if $x$ belongs to $s$.
NonUnitalSubring.mem_mk theorem
{S : NonUnitalSubsemiring R} {x : R} (h) : x ∈ (⟨S, h⟩ : NonUnitalSubring R) ↔ x ∈ S
Full source 
@[simp]
theorem mem_mk {S : NonUnitalSubsemiring R} {x : R} (h) :
    x ∈ (⟨S, h⟩ : NonUnitalSubring R)x ∈ (⟨S, h⟩ : NonUnitalSubring R) ↔ x ∈ S :=
  Iff.rfl
Membership Criterion for Constructed Non-unital Subrings
Informal description
For any non-unital subsemiring $S$ of a non-unital non-associative ring $R$, any element $x \in R$, and any proof $h$ that $S$ is also an additive subgroup, the element $x$ belongs to the constructed non-unital subring $\langle S, h \rangle$ if and only if $x$ belongs to $S$.
NonUnitalSubring.coe_set_mk theorem
(S : NonUnitalSubsemiring R) (h) : ((⟨S, h⟩ : NonUnitalSubring R) : Set R) = S
Full source 
@[simp]
theorem coe_set_mk (S : NonUnitalSubsemiring R) (h) :
    ((⟨S, h⟩ : NonUnitalSubring R) : Set R) = S :=
  rfl
Underlying Set of Non-unital Subring Construction
Informal description
For any non-unital subsemiring $S$ of a non-unital non-associative ring $R$ and any proof $h$ that $S$ is also an additive subgroup, the underlying set of the non-unital subring $\langle S, h \rangle$ is equal to $S$ as a subset of $R$.
NonUnitalSubring.mk_le_mk theorem
{S S' : NonUnitalSubsemiring R} (h h') : (⟨S, h⟩ : NonUnitalSubring R) ≤ (⟨S', h'⟩ : NonUnitalSubring R) ↔ S ≤ S'
Full source 
@[simp]
theorem mk_le_mk {S S' : NonUnitalSubsemiring R} (h h') :
    (⟨S, h⟩ : NonUnitalSubring R) ≤ (⟨S', h'⟩ : NonUnitalSubring R) ↔ S ≤ S' :=
  Iff.rfl
Order Relation Between Constructed Non-unital Subrings
Informal description
Let $S$ and $S'$ be two non-unital subsemirings of a non-unital non-associative ring $R$, with proofs $h$ and $h'$ that they are also additive subgroups. Then the non-unital subring $\langle S, h \rangle$ is contained in $\langle S', h' \rangle$ if and only if $S$ is contained in $S'$ as non-unital subsemirings.
NonUnitalSubring.ext theorem
{S T : NonUnitalSubring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T
Full source 
/-- Two non-unital subrings are equal if they have the same elements. -/
@[ext]
theorem ext {S T : NonUnitalSubring R} (h : ∀ x, x ∈ Sx ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h
Extensionality of Non-unital Subrings
Informal description
Let $S$ and $T$ be two non-unital subrings of a non-unital non-associative ring $R$. If for every element $x \in R$, $x$ belongs to $S$ if and only if $x$ belongs to $T$, then $S$ and $T$ are equal.
NonUnitalSubring.copy definition
(S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubring R
Full source 
/-- Copy of a non-unital subring with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubring R :=
  { S.toNonUnitalSubsemiring.copy s hs with
    carrier := s
    neg_mem' := hs.symm ▸ S.neg_mem' }
Copy of a non-unital subring with specified carrier set
Informal description
Given a non-unital subring $S$ of a non-unital non-associative ring $R$, a subset $s$ of $R$ equal to the underlying set of $S$, and a proof $hs$ that $s$ equals the carrier set of $S$, the function `NonUnitalSubring.copy` constructs a new non-unital subring with carrier set $s$ that is definitionally equal to $S$.
NonUnitalSubring.coe_copy theorem
(S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs : Set R) = s
Full source 
@[simp]
theorem coe_copy (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs : Set R) = s :=
  rfl
Underlying Set of Copied Non-unital Subring Equals Given Set
Informal description
Let $S$ be a non-unital subring of a non-unital non-associative ring $R$, and let $s$ be a subset of $R$ such that $s$ equals the underlying set of $S$. Then the underlying set of the copy of $S$ with carrier set $s$ is equal to $s$ itself.
NonUnitalSubring.copy_eq theorem
(S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S
Full source 
theorem copy_eq (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs
Equality of Copied Non-unital Subring with Original
Informal description
Let $S$ be a non-unital subring of a non-unital non-associative ring $R$, and let $s$ be a subset of $R$ such that $s$ equals the underlying set of $S$. Then the copy of $S$ with carrier set $s$ is equal to $S$ itself.
NonUnitalSubring.toNonUnitalSubsemiring_injective theorem
: Function.Injective (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R)
Full source 
theorem toNonUnitalSubsemiring_injective :
    Function.Injective (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R)
  | _r, _s, h => ext (SetLike.ext_iff.mp h :)
Injectivity of Non-unital Subring to Non-unital Subsemiring Map
Informal description
The function that maps a non-unital subring of a non-unital non-associative ring $R$ to its underlying non-unital subsemiring is injective. That is, if two non-unital subrings $A$ and $B$ of $R$ have the same underlying non-unital subsemiring, then $A = B$.
NonUnitalSubring.toNonUnitalSubsemiring_strictMono theorem
: StrictMono (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R)
Full source 
@[mono]
theorem toNonUnitalSubsemiring_strictMono :
    StrictMono (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R) := fun _ _ =>
  id
Strict Monotonicity of Non-unital Subring to Non-unital Subsemiring Map
Informal description
The function `toNonUnitalSubsemiring` from the type of non-unital subrings of a non-unital non-associative ring $R$ to the type of non-unital subsemirings of $R$ is strictly monotone. That is, for any two non-unital subrings $A$ and $B$ of $R$, if $A \leq B$ in the partial order of non-unital subrings, then the corresponding non-unital subsemiring of $A$ is contained in the non-unital subsemiring of $B$.
NonUnitalSubring.toNonUnitalSubsemiring_mono theorem
: Monotone (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R)
Full source 
@[mono]
theorem toNonUnitalSubsemiring_mono :
    Monotone (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R) :=
  toNonUnitalSubsemiring_strictMono.monotone
Monotonicity of Non-unital Subring to Non-unital Subsemiring Map
Informal description
The function that maps a non-unital subring $A$ of a non-unital non-associative ring $R$ to its underlying non-unital subsemiring is monotone. That is, for any two non-unital subrings $A$ and $B$ of $R$, if $A \leq B$ in the partial order of non-unital subrings, then the corresponding non-unital subsemiring of $A$ is contained in the non-unital subsemiring of $B$.
NonUnitalSubring.toAddSubgroup_injective theorem
: Function.Injective (toAddSubgroup : NonUnitalSubring R → AddSubgroup R)
Full source 
theorem toAddSubgroup_injective :
    Function.Injective (toAddSubgroup : NonUnitalSubring R → AddSubgroup R)
  | _r, _s, h => ext (SetLike.ext_iff.mp h :)
Injectivity of the Underlying Additive Subgroup Map for Non-unital Subrings
Informal description
The function that maps a non-unital subring $S$ of a non-unital non-associative ring $R$ to its underlying additive subgroup is injective. That is, if two non-unital subrings $S$ and $T$ of $R$ have the same underlying additive subgroup, then $S = T$.
NonUnitalSubring.toAddSubgroup_strictMono theorem
: StrictMono (toAddSubgroup : NonUnitalSubring R → AddSubgroup R)
Full source 
@[mono]
theorem toAddSubgroup_strictMono :
    StrictMono (toAddSubgroup : NonUnitalSubring R → AddSubgroup R) := fun _ _ => id
Strict Monotonicity of the Underlying Additive Subgroup Map for Non-unital Subrings
Informal description
The function that maps a non-unital subring $S$ of a non-unital non-associative ring $R$ to its underlying additive subgroup is strictly monotone. That is, for any two non-unital subrings $S$ and $T$ of $R$, if $S < T$ in the partial order of non-unital subrings, then the corresponding additive subgroup of $S$ is strictly contained in the additive subgroup of $T$.
NonUnitalSubring.toAddSubgroup_mono theorem
: Monotone (toAddSubgroup : NonUnitalSubring R → AddSubgroup R)
Full source 
@[mono]
theorem toAddSubgroup_mono : Monotone (toAddSubgroup : NonUnitalSubring R → AddSubgroup R) :=
  toAddSubgroup_strictMono.monotone
Monotonicity of the Underlying Additive Subgroup Map for Non-unital Subrings
Informal description
The function that maps a non-unital subring $S$ of a non-unital non-associative ring $R$ to its underlying additive subgroup is monotone. That is, for any two non-unital subrings $S$ and $T$ of $R$, if $S \leq T$ in the partial order of non-unital subrings, then the corresponding additive subgroup of $S$ is contained in the additive subgroup of $T$.
NonUnitalSubring.toSubsemigroup_injective theorem
: Function.Injective (toSubsemigroup : NonUnitalSubring R → Subsemigroup R)
Full source 
theorem toSubsemigroup_injective :
    Function.Injective (toSubsemigroup : NonUnitalSubring R → Subsemigroup R)
  | _r, _s, h => ext (SetLike.ext_iff.mp h :)
Injectivity of the Underlying Multiplicative Subsemigroup Map for Non-unital Subrings
Informal description
The function that maps a non-unital subring $S$ of a non-unital non-associative ring $R$ to its underlying multiplicative subsemigroup is injective. That is, if two non-unital subrings $S$ and $T$ have the same underlying multiplicative subsemigroup, then $S = T$.
NonUnitalSubring.toSubsemigroup_strictMono theorem
: StrictMono (toSubsemigroup : NonUnitalSubring R → Subsemigroup R)
Full source 
@[mono]
theorem toSubsemigroup_strictMono :
    StrictMono (toSubsemigroup : NonUnitalSubring R → Subsemigroup R) := fun _ _ => id
Strict Monotonicity of the Underlying Multiplicative Subsemigroup Map for Non-unital Subrings
Informal description
The function that maps a non-unital subring $S$ of a non-unital non-associative ring $R$ to its underlying multiplicative subsemigroup is strictly monotone with respect to the partial order on non-unital subrings induced by inclusion.
NonUnitalSubring.toSubsemigroup_mono theorem
: Monotone (toSubsemigroup : NonUnitalSubring R → Subsemigroup R)
Full source 
@[mono]
theorem toSubsemigroup_mono : Monotone (toSubsemigroup : NonUnitalSubring R → Subsemigroup R) :=
  toSubsemigroup_strictMono.monotone
Monotonicity of the Underlying Multiplicative Subsemigroup Map for Non-unital Subrings
Informal description
The function that maps a non-unital subring $S$ of a non-unital non-associative ring $R$ to its underlying multiplicative subsemigroup is monotone with respect to the partial order on non-unital subrings induced by inclusion.
NonUnitalSubring.mk' definition
(s : Set R) (sm : Subsemigroup R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : NonUnitalSubring R
Full source 
/-- Construct a `NonUnitalSubring R` from a set `s`, a subsemigroup `sm`, and an additive
subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/
protected def mk' (s : Set R) (sm : Subsemigroup R) (sa : AddSubgroup R) (hm : ↑sm = s)
    (ha : ↑sa = s) : NonUnitalSubring R :=
  { sm.copy s hm.symm, sa.copy s ha.symm with }
Construction of a non-unital subring from matching subsemigroup and additive subgroup
Informal description
Given a subset $s$ of a non-unital non-associative ring $R$, a subsemigroup $sm$ of $R$, and an additive subgroup $sa$ of $R$ such that the carrier sets of $sm$ and $sa$ both equal $s$, the function constructs a non-unital subring of $R$ with underlying set $s$.
NonUnitalSubring.coe_mk' theorem
{s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha : Set R) = s
Full source 
@[simp]
theorem coe_mk' {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
    (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha : Set R) = s :=
  rfl
Underlying Set of Constructed Non-unital Subring Equals Input Set
Informal description
Given a subset $s$ of a non-unital non-associative ring $R$, a subsemigroup $sm$ of $R$, and an additive subgroup $sa$ of $R$ such that the carrier sets of $sm$ and $sa$ both equal $s$, the underlying set of the non-unital subring constructed via `NonUnitalSubring.mk' s sm sa hm ha` is equal to $s$.
NonUnitalSubring.mem_mk' theorem
{s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} : x ∈ NonUnitalSubring.mk' s sm sa hm ha ↔ x ∈ s
Full source 
@[simp]
theorem mem_mk' {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s)
    {x : R} : x ∈ NonUnitalSubring.mk' s sm sa hm hax ∈ NonUnitalSubring.mk' s sm sa hm ha ↔ x ∈ s :=
  Iff.rfl
Membership in Constructed Non-unital Subring via Matching Substructures
Informal description
Let $R$ be a non-unital non-associative ring, $s$ a subset of $R$, $sm$ a subsemigroup of $R$, and $sa$ an additive subgroup of $R$ such that the carrier sets of $sm$ and $sa$ both equal $s$. For any element $x \in R$, we have $x$ belongs to the non-unital subring constructed via `NonUnitalSubring.mk' s sm sa hm ha` if and only if $x$ belongs to $s$.
NonUnitalSubring.mk'_toSubsemigroup theorem
{s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm
Full source 
@[simp]
theorem mk'_toSubsemigroup {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
    (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm :=
  SetLike.coe_injective hm.symm
Underlying Subsemigroup of Constructed Non-unital Subring
Informal description
Given a subset $s$ of a non-unital non-associative ring $R$, a subsemigroup $sm$ of $R$, and an additive subgroup $sa$ of $R$ such that the carrier sets of $sm$ and $sa$ both equal $s$, the underlying multiplicative subsemigroup of the constructed non-unital subring equals $sm$.
NonUnitalSubring.mk'_toAddSubgroup theorem
{s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa
Full source 
@[simp]
theorem mk'_toAddSubgroup {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
    (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa :=
  SetLike.coe_injective ha.symm
Underlying Additive Subgroup of Constructed Non-unital Subring
Informal description
Given a subset $s$ of a non-unital non-associative ring $R$, a subsemigroup $sm$ of $R$, and an additive subgroup $sa$ of $R$ such that the carrier sets of $sm$ and $sa$ both equal $s$, the underlying additive subgroup of the constructed non-unital subring equals $sa$.
NonUnitalSubring.zero_mem theorem
: (0 : R) ∈ s
Full source 
/-- A non-unital subring contains the ring's 0. -/
protected theorem zero_mem : (0 : R) ∈ s :=
  zero_mem _
Zero Element Belongs to Non-unital Subring
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, the zero element $0$ is contained in $s$.
NonUnitalSubring.mul_mem theorem
{x y : R} : x ∈ s → y ∈ s → x * y ∈ s
Full source 
/-- A non-unital subring is closed under multiplication. -/
protected theorem mul_mem {x y : R} : x ∈ s → y ∈ s → x * y ∈ s :=
  mul_mem
Closure of Non-unital Subring under Multiplication
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, and for any elements $x, y \in R$ such that $x \in s$ and $y \in s$, the product $x * y$ belongs to $s$.
NonUnitalSubring.add_mem theorem
{x y : R} : x ∈ s → y ∈ s → x + y ∈ s
Full source 
/-- A non-unital subring is closed under addition. -/
protected theorem add_mem {x y : R} : x ∈ s → y ∈ s → x + y ∈ s :=
  add_mem
Closure of Non-unital Subring under Addition
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, and for any elements $x, y \in R$ such that $x \in s$ and $y \in s$, the sum $x + y$ belongs to $s$.
NonUnitalSubring.neg_mem theorem
{x : R} : x ∈ s → -x ∈ s
Full source 
/-- A non-unital subring is closed under negation. -/
protected theorem neg_mem {x : R} : x ∈ s → -x ∈ s :=
  neg_mem
Closure of Non-unital Subring under Negation
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, and for any element $x \in R$ such that $x \in s$, the negation $-x$ belongs to $s$.
NonUnitalSubring.sub_mem theorem
{x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s
Full source 
/-- A non-unital subring is closed under subtraction -/
protected theorem sub_mem {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s :=
  sub_mem hx hy
Closure of Non-unital Subring under Subtraction
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, and for any elements $x, y \in R$ such that $x \in s$ and $y \in s$, the difference $x - y$ belongs to $s$.
NonUnitalSubring.toNonUnitalRing instance
{R : Type*} [NonUnitalRing R] (s : NonUnitalSubring R) : NonUnitalRing s
Full source 
/-- A non-unital subring of a non-unital ring inherits a non-unital ring structure -/
instance toNonUnitalRing {R : Type*} [NonUnitalRing R] (s : NonUnitalSubring R) :
    NonUnitalRing s := fast_instance%
  Subtype.coe_injective.nonUnitalRing _ rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Non-unital Subrings Inherit Non-unital Ring Structure
Informal description
For any non-unital ring $R$ and any non-unital subring $s$ of $R$, $s$ inherits a non-unital ring structure from $R$.
NonUnitalSubring.zsmul_mem theorem
{x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s
Full source 
protected theorem zsmul_mem {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s :=
  zsmul_mem hx n
Closure of Non-unital Subring under Integer Scalar Multiplication
Informal description
For any non-unital subring $s$ of a non-unital ring $R$, if an element $x \in R$ belongs to $s$, then for any integer $n$, the scalar multiple $n \cdot x$ also belongs to $s$.
NonUnitalSubring.val_add theorem
(x y : s) : (↑(x + y) : R) = ↑x + ↑y
Full source 
@[simp, norm_cast]
theorem val_add (x y : s) : (↑(x + y) : R) = ↑x + ↑y :=
  rfl
Addition in Non-unital Subring Preserves Canonical Inclusion
Informal description
For any elements $x$ and $y$ in a non-unital subring $s$ of a non-unital non-associative ring $R$, the image of their sum under the canonical inclusion map equals the sum of their images in $R$, i.e., $(x + y) = x + y$ where the left-hand side is computed in $s$ and the right-hand side in $R$.
NonUnitalSubring.val_neg theorem
(x : s) : (↑(-x) : R) = -↑x
Full source 
@[simp, norm_cast]
theorem val_neg (x : s) : (↑(-x) : R) = -↑x :=
  rfl
Negation Preservation in Non-unital Subring Inclusion
Informal description
For any element $x$ in a non-unital subring $s$ of a non-unital non-associative ring $R$, the image of the negation of $x$ under the canonical inclusion map equals the negation of the image of $x$ in $R$, i.e., $(-x) = -x$ where the left-hand side is computed in $s$ and the right-hand side in $R$.
NonUnitalSubring.val_mul theorem
(x y : s) : (↑(x * y) : R) = ↑x * ↑y
Full source 
@[simp, norm_cast]
theorem val_mul (x y : s) : (↑(x * y) : R) = ↑x * ↑y :=
  rfl
Multiplication in Non-unital Subring Preserves Canonical Inclusion
Informal description
For any elements $x$ and $y$ in a non-unital subring $s$ of a non-unital non-associative ring $R$, the image of their product under the canonical inclusion map equals the product of their images in $R$, i.e., $(x \cdot y) = x \cdot y$ where the left-hand side is computed in $s$ and the right-hand side in $R$.
NonUnitalSubring.val_zero theorem
: ((0 : s) : R) = 0
Full source 
@[simp, norm_cast]
theorem val_zero : ((0 : s) : R) = 0 :=
  rfl
Zero Preservation in Non-unital Subring Inclusion
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, the image of the zero element of $s$ under the canonical inclusion map equals the zero element of $R$, i.e., $(0 : s) = 0$ where the left-hand side is evaluated in $R$.
NonUnitalSubring.coe_eq_zero_iff theorem
{x : s} : (x : R) = 0 ↔ x = 0
Full source 
theorem coe_eq_zero_iff {x : s} : (x : R) = 0 ↔ x = 0 := by
  simp
Zero Criterion via Canonical Inclusion in Non-unital Subrings
Informal description
For any element $x$ in a non-unital subring $s$ of a non-unital non-associative ring $R$, the image of $x$ under the canonical inclusion map equals zero in $R$ if and only if $x$ is the zero element in $s$. In other words, $(x : R) = 0 \leftrightarrow x = 0$ where the left-hand side is evaluated in $R$ and the right-hand side in $s$.
NonUnitalSubring.toNonUnitalCommRing instance
{R} [NonUnitalCommRing R] (s : NonUnitalSubring R) : NonUnitalCommRing s
Full source 
/-- A non-unital subring of a `NonUnitalCommRing` is a `NonUnitalCommRing`. -/
instance toNonUnitalCommRing {R} [NonUnitalCommRing R] (s : NonUnitalSubring R) :
    NonUnitalCommRing s := fast_instance%
  Subtype.coe_injective.nonUnitalCommRing _ rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Non-unital Subrings Inherit Non-unital Commutative Ring Structure
Informal description
For any non-unital commutative ring $R$ and any non-unital subring $s$ of $R$, $s$ inherits a non-unital commutative ring structure from $R$.
NonUnitalSubring.mem_toSubsemigroup theorem
{s : NonUnitalSubring R} {x : R} : x ∈ s.toSubsemigroup ↔ x ∈ s
Full source 
@[simp]
theorem mem_toSubsemigroup {s : NonUnitalSubring R} {x : R} : x ∈ s.toSubsemigroupx ∈ s.toSubsemigroup ↔ x ∈ s :=
  Iff.rfl
Membership in Non-unital Subring and its Multiplicative Subsemigroup
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$ and any element $x \in R$, $x$ belongs to the underlying multiplicative subsemigroup of $s$ if and only if $x$ belongs to $s$.
NonUnitalSubring.coe_toSubsemigroup theorem
(s : NonUnitalSubring R) : (s.toSubsemigroup : Set R) = s
Full source 
@[simp]
theorem coe_toSubsemigroup (s : NonUnitalSubring R) : (s.toSubsemigroup : Set R) = s :=
  rfl
Equality of Non-unital Subring and its Multiplicative Subsemigroup
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, the underlying set of the multiplicative subsemigroup associated with $s$ is equal to $s$ itself, i.e., $s.\text{toSubsemigroup} = s$ as sets.
NonUnitalSubring.mem_toAddSubgroup theorem
{s : NonUnitalSubring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s
Full source 
@[simp]
theorem mem_toAddSubgroup {s : NonUnitalSubring R} {x : R} : x ∈ s.toAddSubgroupx ∈ s.toAddSubgroup ↔ x ∈ s :=
  Iff.rfl
Membership in Non-unital Subring and its Additive Subgroup Coincide
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$ and any element $x \in R$, $x$ belongs to the underlying additive subgroup of $s$ if and only if $x$ belongs to $s$.
NonUnitalSubring.coe_toAddSubgroup theorem
(s : NonUnitalSubring R) : (s.toAddSubgroup : Set R) = s
Full source 
@[simp]
theorem coe_toAddSubgroup (s : NonUnitalSubring R) : (s.toAddSubgroup : Set R) = s :=
  rfl
Equality of Non-unital Subring and its Additive Subgroup
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, the underlying set of the additive subgroup associated with $s$ is equal to $s$ itself, i.e., $s.\text{toAddSubgroup} = s$ as sets.
NonUnitalSubring.mem_toNonUnitalSubsemiring theorem
{s : NonUnitalSubring R} {x : R} : x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s
Full source 
@[simp]
theorem mem_toNonUnitalSubsemiring {s : NonUnitalSubring R} {x : R} :
    x ∈ s.toNonUnitalSubsemiringx ∈ s.toNonUnitalSubsemiring ↔ x ∈ s :=
  Iff.rfl
Membership in Non-unital Subring and its Underlying Non-unital Subsemiring Coincide
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$ and any element $x \in R$, $x$ belongs to the underlying non-unital subsemiring of $s$ if and only if $x$ belongs to $s$.
NonUnitalSubring.coe_toNonUnitalSubsemiring theorem
(s : NonUnitalSubring R) : (s.toNonUnitalSubsemiring : Set R) = s
Full source 
@[simp]
theorem coe_toNonUnitalSubsemiring (s : NonUnitalSubring R) :
    (s.toNonUnitalSubsemiring : Set R) = s :=
  rfl
Equality of Non-unital Subring and its Underlying Non-unital Subsemiring
Informal description
For any non-unital subring $s$ of a non-unital non-associative ring $R$, the underlying set of the non-unital subsemiring associated with $s$ is equal to $s$ itself.
NonUnitalSubring.inclusion definition
{S T : NonUnitalSubring R} (h : S ≤ T) : S →ₙ+* T
Full source 
/-- The ring homomorphism associated to an inclusion of `NonUnitalSubring`s. -/
def inclusion {S T : NonUnitalSubring R} (h : S ≤ T) : S →ₙ+* T :=
  NonUnitalRingHom.codRestrict (NonUnitalSubringClass.subtype S) _ fun x => h x.2
Inclusion homomorphism between non-unital subrings
Informal description
Given two non-unital subrings \( S \) and \( T \) of a non-unital non-associative ring \( R \) such that \( S \subseteq T \), the inclusion map \( S \hookrightarrow T \) is a non-unital ring homomorphism.