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 thefield
typeclass; thefield
typeclass is a constructive mathematics version ofdiscrete_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.