mathlib documentation

algebra.group_with_zero.defs

Typeclasses for groups with an adjoined zero element #

This file provides just the typeclass definitions, and the projection lemmas that expose their members.

Main definitions #

source
@[instance]
def mul_zero_class.to_has_mul (M₀ : Type u_4) [s : mul_zero_class M₀] :
has_mul M₀
source
@[class]
structure mul_zero_class (M₀ : Type u_4) :
Type u_4
  • mul : M₀ → M₀ → M₀
  • zero : M₀
  • zero_mul : ∀ (a : M₀), 0 * a = 0
  • mul_zero : ∀ (a : M₀), a * 0 = 0

Typeclass for expressing that a type M₀ with multiplication and a zero satisfies 0 * a = 0 and a * 0 = 0 for all a : M₀.

Instances
source
@[instance]
def mul_zero_class.to_has_zero (M₀ : Type u_4) [s : mul_zero_class M₀] :
has_zero M₀
source
@[simp]
theorem zero_mul {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
0 * a = 0
source
@[simp]
theorem mul_zero {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
a * 0 = 0
source
@[class]
structure no_zero_divisors (M₀ : Type u_4) [has_mul M₀] [has_zero M₀] :
Prop
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0

Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0 for all a and b of type G₀.

Instances
source
@[instance]
def monoid_with_zero.to_mul_zero_class (M₀ : Type u_4) [s : monoid_with_zero M₀] :
mul_zero_class M₀
source
@[instance]
def monoid_with_zero.to_monoid (M₀ : Type u_4) [s : monoid_with_zero M₀] :
monoid M₀
source
@[class]
structure monoid_with_zero (M₀ : Type u_4) :
Type u_4
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : M₀
  • one_mul : ∀ (a : M₀), 1 * a = a
  • mul_one : ∀ (a : M₀), a * 1 = a
  • zero : M₀
  • zero_mul : ∀ (a : M₀), 0 * a = 0
  • mul_zero : ∀ (a : M₀), a * 0 = 0

A type M is a “monoid with zero” if it is a monoid with zero element, and 0 is left and right absorbing.

Instances
source
@[instance]
def cancel_monoid_with_zero.to_monoid_with_zero (M₀ : Type u_4) [s : cancel_monoid_with_zero M₀] :
monoid_with_zero M₀
source
@[class]
structure cancel_monoid_with_zero (M₀ : Type u_4) :
Type u_4
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : M₀
  • one_mul : ∀ (a : M₀), 1 * a = a
  • mul_one : ∀ (a : M₀), a * 1 = a
  • zero : M₀
  • zero_mul : ∀ (a : M₀), 0 * a = 0
  • mul_zero : ∀ (a : M₀), a * 0 = 0
  • mul_left_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, a ≠ 0 → a * b = a * c_1 → b = c_1
  • mul_right_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, b ≠ 0 → a * b = c_1 * b → a = c_1

A type M is a cancel_monoid_with_zero if it is a monoid with zero element, 0 is left and right absorbing, and left/right multiplication by a non-zero element is injective.

Instances
source
theorem mul_left_cancel' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} (ha : a ≠ 0) (h : a * b = a * c) :
b = c
source
theorem mul_right_cancel' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} (hb : b ≠ 0) (h : a * b = c * b) :
a = c
source
theorem mul_right_injective' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a : M₀} (ha : a ≠ 0) :
function.injective (has_mul.mul a)
source
theorem mul_left_injective' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {b : M₀} (hb : b ≠ 0) :
function.injective (λ (a : M₀), a * b)
source
@[instance]
def comm_monoid_with_zero.to_comm_monoid (M₀ : Type u_4) [s : comm_monoid_with_zero M₀] :
comm_monoid M₀
source
@[instance]
def comm_monoid_with_zero.to_monoid_with_zero (M₀ : Type u_4) [s : comm_monoid_with_zero M₀] :
monoid_with_zero M₀
source
@[class]
structure comm_monoid_with_zero (M₀ : Type u_4) :
Type u_4
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : M₀
  • one_mul : ∀ (a : M₀), 1 * a = a
  • mul_one : ∀ (a : M₀), a * 1 = a
  • mul_comm : ∀ (a b : M₀), a * b = b * a
  • zero : M₀
  • zero_mul : ∀ (a : M₀), 0 * a = 0
  • mul_zero : ∀ (a : M₀), a * 0 = 0

A type M is a commutative “monoid with zero” if it is a commutative monoid with zero element, and 0 is left and right absorbing.

Instances
source
@[instance]
def comm_cancel_monoid_with_zero.to_cancel_monoid_with_zero (M₀ : Type u_4) [s : comm_cancel_monoid_with_zero M₀] :
cancel_monoid_with_zero M₀
source
@[instance]
def comm_cancel_monoid_with_zero.to_comm_monoid_with_zero (M₀ : Type u_4) [s : comm_cancel_monoid_with_zero M₀] :
comm_monoid_with_zero M₀
source
@[class]
structure comm_cancel_monoid_with_zero (M₀ : Type u_4) :
Type u_4
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : M₀
  • one_mul : ∀ (a : M₀), 1 * a = a
  • mul_one : ∀ (a : M₀), a * 1 = a
  • mul_comm : ∀ (a b : M₀), a * b = b * a
  • zero : M₀
  • zero_mul : ∀ (a : M₀), 0 * a = 0
  • mul_zero : ∀ (a : M₀), a * 0 = 0
  • mul_left_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, a ≠ 0 → a * b = a * c_1 → b = c_1
  • mul_right_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, b ≠ 0 → a * b = c_1 * b → a = c_1

A type M is a comm_cancel_monoid_with_zero if it is a commutative monoid with zero element, 0 is left and right absorbing, and left/right multiplication by a non-zero element is injective.

Instances
source
@[instance]
def group_with_zero.to_nontrivial (G₀ : Type u) [s : group_with_zero G₀] :
nontrivial G₀
source
@[instance]
def group_with_zero.to_monoid_with_zero (G₀ : Type u) [s : group_with_zero G₀] :
monoid_with_zero G₀
source
@[class]
structure group_with_zero (G₀ : Type u) :
Type u
  • mul : G₀ → G₀ → G₀
  • mul_assoc : ∀ (a b c_1 : G₀), (a * b) * c_1 = a * b * c_1
  • one : G₀
  • one_mul : ∀ (a : G₀), 1 * a = a
  • mul_one : ∀ (a : G₀), a * 1 = a
  • zero : G₀
  • zero_mul : ∀ (a : G₀), 0 * a = 0
  • mul_zero : ∀ (a : G₀), a * 0 = 0
  • inv : G₀ → G₀
  • div : G₀ → G₀ → G₀
  • div_eq_mul_inv : (∀ (a b : G₀), a / b = a * b⁻¹) . "try_refl_tac"
  • exists_pair_ne : ∃ (x y : G₀), x ≠ y
  • inv_zero : 0⁻¹ = 0
  • mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1

A type G₀ is a “group with zero” if it is a monoid with zero element (distinct from 1) such that every nonzero element is invertible. The type is required to come with an “inverse” function, and the inverse of 0 must be 0.

Examples include division rings and the ordered monoids that are the target of valuations in general valuation theory.

Instances
source
@[instance]
def group_with_zero.to_div_inv_monoid (G₀ : Type u) [s : group_with_zero G₀] :
div_inv_monoid G₀
source
@[simp]
theorem inv_zero {G₀ : Type u} [group_with_zero G₀] :
0⁻¹ = 0
source
@[simp]
theorem mul_inv_cancel {G₀ : Type u} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :
a * a⁻¹ = 1
source
@[class]
structure comm_group_with_zero (G₀ : Type u_4) :
Type u_4
  • mul : G₀ → G₀ → G₀
  • mul_assoc : ∀ (a b c_1 : G₀), (a * b) * c_1 = a * b * c_1
  • one : G₀
  • one_mul : ∀ (a : G₀), 1 * a = a
  • mul_one : ∀ (a : G₀), a * 1 = a
  • mul_comm : ∀ (a b : G₀), a * b = b * a
  • zero : G₀
  • zero_mul : ∀ (a : G₀), 0 * a = 0
  • mul_zero : ∀ (a : G₀), a * 0 = 0
  • inv : G₀ → G₀
  • div : G₀ → G₀ → G₀
  • div_eq_mul_inv : (∀ (a b : G₀), a / b = a * b⁻¹) . "try_refl_tac"
  • exists_pair_ne : ∃ (x y : G₀), x ≠ y
  • inv_zero : 0⁻¹ = 0
  • mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1

A type G₀ is a commutative “group with zero” if it is a commutative monoid with zero element (distinct from 1) such that every nonzero element is invertible. The type is required to come with an “inverse” function, and the inverse of 0 must be 0.

Instances
source
@[instance]
def comm_group_with_zero.to_group_with_zero (G₀ : Type u_4) [s : comm_group_with_zero G₀] :
group_with_zero G₀
source
@[instance]
def comm_group_with_zero.to_comm_monoid_with_zero (G₀ : Type u_4) [s : comm_group_with_zero G₀] :
comm_monoid_with_zero G₀