Generating elements of rings

Content created by Egbert Rijke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2023-09-21.

module ring-theory.generating-elements-rings where
Imports 
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

Recent changes