# Maths in Lean : rings and fields.

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.