This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Generating elements of rings

module ring-theory.generating-elements-rings where

open import foundation.propositions
open import foundation.universe-levels

open import group-theory.generating-elements-groups

open import ring-theory.rings

Idea

A generating element of a ring R is an element g which is a generating element of the underlying additive group of R. That is, g is a generating element of a ring R if for every element x : R there exists an integer k such that kg ＝ x.

Definitions

Generating elements of a ring

module _
  {l : Level} (R : Ring l) (g : type-Ring R)
  where

  is-generating-element-prop-Ring : Prop l
  is-generating-element-prop-Ring =
    is-generating-element-prop-Group (group-Ring R) g