The `ring`

typeclass is defined in the core library, in `init/algebra/ring`

. Related typeclasses are also defined in the `init/algebra`

directory.

## Basic typeclasses.

`ring`

(note that in Lean a ring automatically has a 1)`comm_ring`

(a commutative ring)`integral_domain`

`division_ring`

`discrete_field`

(note that mathematicians will probably want to use this typeclass for fields, rather than the`field`

typeclass; the`field`

typeclass is a constructive mathematics version of`discrete_field`

).

## Usage examples.

variable (R₁ : Type*) variable [ring R₁] example : ∀ r : R₁, r+1=1+r := λ r, add_comm r 1 example : ∀ r : R₁, r * 1 = r := mul_one variable (R₂ : Type*) variable [comm_ring R₂] example : ∀ (a b : R₂), a * a - b * b = (a + b) * (a - b) := mul_self_sub_mul_self_eq example (a b c : R₂) (h : a ∣ b) : a ∣ c ↔ a ∣ b + c := dvd_add_iff_right h variable (R₃ : Type*) variable [integral_domain R₃] example (a b : R₃) : a * b = 0 ↔ a = 0 ∨ b = 0 := mul_eq_zero_iff_eq_zero_or_eq_zero example (a b : R₃) : b ≠ 1 → a * b = a → a = 0 := eq_zero_of_mul_eq_self_right variable (F : Type*) variable [field F] example (a b c : F) : (a / c) - (b / c) = (a - b) / c := div_sub_div_same a b c example (a b : F) (hb : b ≠ 0) : a / b = 1 ↔ a = b := div_eq_one_iff_eq a hb

### Related typeclasses.

`discrete_linear_ordered_field`

etc.

Advertisements