mathlib3 documentation

algebra.group_with_zero.defs

Typeclasses for groups with an adjoined zero element #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

@[instance]
def mul_zero_class.to_has_mul (M₀ : Type u_4) [self : mul_zero_class M₀] :
has_mul M₀
@[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 of this typeclass
Instances of other typeclasses for mul_zero_class
  • mul_zero_class.has_sizeof_inst
@[instance]
def mul_zero_class.to_has_zero (M₀ : Type u_4) [self : mul_zero_class M₀] :
@[simp]
theorem zero_mul {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
0 * a = 0
@[simp]
theorem mul_zero {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
a * 0 = 0
@[class]
structure is_left_cancel_mul_zero (M₀ : Type u) [has_mul M₀] [has_zero M₀] :
Prop
  • mul_left_cancel_of_ne_zero : {a b c : M₀}, a 0 a * b = a * c b = c

A mixin for left cancellative multiplication by nonzero elements.

Instances of this typeclass
theorem mul_left_cancel₀ {M₀ : Type u_1} [has_mul M₀] [has_zero M₀] [is_left_cancel_mul_zero M₀] {a b c : M₀} (ha : a 0) (h : a * b = a * c) :
b = c
theorem mul_right_injective₀ {M₀ : Type u_1} [has_mul M₀] [has_zero M₀] [is_left_cancel_mul_zero M₀] {a : M₀} (ha : a 0) :
@[class]
structure is_right_cancel_mul_zero (M₀ : Type u) [has_mul M₀] [has_zero M₀] :
Prop
  • mul_right_cancel_of_ne_zero : {a b c : M₀}, b 0 a * b = c * b a = c

A mixin for right cancellative multiplication by nonzero elements.

Instances of this typeclass
theorem mul_right_cancel₀ {M₀ : Type u_1} [has_mul M₀] [has_zero M₀] [is_right_cancel_mul_zero M₀] {a b c : M₀} (hb : b 0) (h : a * b = c * b) :
a = c
theorem mul_left_injective₀ {M₀ : Type u_1} [has_mul M₀] [has_zero M₀] [is_right_cancel_mul_zero M₀] {b : M₀} (hb : b 0) :
function.injective (λ (a : M₀), a * b)
@[class]
structure is_cancel_mul_zero (M₀ : Type u) [has_mul M₀] [has_zero M₀] :
Prop
  • mul_left_cancel_of_ne_zero : {a b c : M₀}, a 0 a * b = a * c b = c
  • mul_right_cancel_of_ne_zero : {a b c : M₀}, b 0 a * b = c * b a = c

A mixin for cancellative multiplication by nonzero elements.

Instances of this typeclass
@[class]
structure semigroup_with_zero (S₀ : Type u_4) :
Type u_4
  • mul : S₀ S₀ S₀
  • mul_assoc : (a b c : S₀), a * b * c = a * (b * c)
  • zero : S₀
  • zero_mul : (a : S₀), 0 * a = 0
  • mul_zero : (a : S₀), a * 0 = 0

A type S₀ is a "semigroup with zero” if it is a semigroup with zero element, and 0 is left and right absorbing.

Instances of this typeclass
Instances of other typeclasses for semigroup_with_zero
  • semigroup_with_zero.has_sizeof_inst
@[instance]
@[instance]
def semigroup_with_zero.to_semigroup (S₀ : Type u_4) [self : semigroup_with_zero S₀] :
@[class]
structure mul_zero_one_class (M₀ : Type u_4) :
Type u_4
  • one : M₀
  • mul : M₀ M₀ 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 typeclass for non-associative monoids with zero elements.

Instances of this typeclass
Instances of other typeclasses for mul_zero_one_class
  • mul_zero_one_class.has_sizeof_inst
@[instance]
@[instance]
@[instance]
@[instance]
def monoid_with_zero.to_monoid (M₀ : Type u_4) [self : monoid_with_zero M₀] :
monoid M₀
@[class]
structure monoid_with_zero (M₀ : Type u_4) :
Type u_4

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

Instances of this typeclass
Instances of other typeclasses for monoid_with_zero
  • monoid_with_zero.has_sizeof_inst
@[class]
structure cancel_monoid_with_zero (M₀ : Type u_4) :
Type u_4

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 of this typeclass
Instances of other typeclasses for cancel_monoid_with_zero
  • cancel_monoid_with_zero.has_sizeof_inst
@[instance]
@[class]
structure comm_monoid_with_zero (M₀ : Type u_4) :
Type u_4

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 of this typeclass
Instances of other typeclasses for comm_monoid_with_zero
  • comm_monoid_with_zero.has_sizeof_inst
@[class]
structure cancel_comm_monoid_with_zero (M₀ : Type u_4) :
Type u_4

A type M is a cancel_comm_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 of this typeclass
Instances of other typeclasses for cancel_comm_monoid_with_zero
  • cancel_comm_monoid_with_zero.has_sizeof_inst
@[instance]
def group_with_zero.to_nontrivial (G₀ : Type u) [self : group_with_zero G₀] :
@[instance]
@[class]
structure group_with_zero (G₀ : Type u) :

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 of this typeclass
Instances of other typeclasses for group_with_zero
  • group_with_zero.has_sizeof_inst
@[instance]
@[simp]
theorem inv_zero {G₀ : Type u} [group_with_zero G₀] :
0⁻¹ = 0
@[simp]
theorem mul_inv_cancel {G₀ : Type u} [group_with_zero G₀] {a : G₀} (h : a 0) :
a * a⁻¹ = 1
@[class]
structure comm_group_with_zero (G₀ : Type u_4) :
Type u_4

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 of this typeclass
Instances of other typeclasses for comm_group_with_zero
  • comm_group_with_zero.has_sizeof_inst
@[instance]
@[protected, instance]
def ne_zero.one (M₀ : Type u_1) [mul_zero_one_class M₀] [nontrivial M₀] :

In a nontrivial monoid with zero, zero and one are different.

theorem pullback_nonzero {M₀ : Type u_1} {M₀' : Type u_2} [mul_zero_one_class M₀] [nontrivial M₀] [has_zero M₀'] [has_one M₀'] (f : M₀' M₀) (zero : f 0 = 0) (one : f 1 = 1) :

Pullback a nontrivial instance along a function sending 0 to 0 and 1 to 1.

theorem mul_eq_zero_of_left {M₀ : Type u_1} [mul_zero_class M₀] {a : M₀} (h : a = 0) (b : M₀) :
a * b = 0
theorem mul_eq_zero_of_right {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) {b : M₀} (h : b = 0) :
a * b = 0
@[simp]
theorem mul_eq_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :
a * b = 0 a = 0 b = 0

If α has no zero divisors, then the product of two elements equals zero iff one of them equals zero.

@[simp]
theorem zero_eq_mul {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :
0 = a * b a = 0 b = 0

If α has no zero divisors, then the product of two elements equals zero iff one of them equals zero.

theorem mul_ne_zero_iff {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :
a * b 0 a 0 b 0

If α has no zero divisors, then the product of two elements is nonzero iff both of them are nonzero.

theorem mul_eq_zero_comm {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :
a * b = 0 b * a = 0

If α has no zero divisors, then for elements a, b : α, a * b equals zero iff so is b * a.

theorem mul_ne_zero_comm {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :
a * b 0 b * a 0

If α has no zero divisors, then for elements a, b : α, a * b is nonzero iff so is b * a.

theorem mul_self_eq_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
a * a = 0 a = 0
theorem zero_eq_mul_self {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
0 = a * a a = 0
theorem mul_self_ne_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
a * a 0 a 0
theorem zero_ne_mul_self {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
0 a * a a 0