mathlib3 documentation

algebra.group_with_zero.basic

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 describes structures that are not usually studied on their own right in mathematics, namely a special sort of monoid: apart from a distinguished “zero element” they form a group, or in other words, they are groups with an adjoined zero element.

Examples are:

division rings;
the value monoid of a multiplicative valuation;
in particular, the non-negative real numbers.

Main definitions #

Various lemmas about group_with_zero and comm_group_with_zero. To reduce import dependencies, the type-classes themselves are in algebra.group_with_zero.defs.

Implementation details #

As is usual in mathlib, we extend the inverse function to the zero element, and require 0⁻¹ = 0.

theorem left_ne_zero_of_mul {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} :

a * b ≠ 0 → a ≠ 0

theorem right_ne_zero_of_mul {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} :

a * b ≠ 0 → b ≠ 0

theorem ne_zero_and_ne_zero_of_mul {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} (h : a * b ≠ 0) :

a ≠ 0 ∧ b ≠ 0

theorem mul_eq_zero_of_ne_zero_imp_eq_zero {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} (h : a ≠ 0 → b = 0) :

a * b = 0

theorem zero_mul_eq_const {M₀ : Type u_2} [mul_zero_class M₀] :

has_mul.mul 0 = function.const M₀ 0

To match one_mul_eq_id.

theorem mul_zero_eq_const {M₀ : Type u_2} [mul_zero_class M₀] :

(λ (_x : M₀), _x * 0) = function.const M₀ 0

To match mul_one_eq_id.

theorem eq_zero_of_mul_self_eq_zero {M₀ : Type u_2} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a : M₀} (h : a * a = 0) :

a = 0

theorem mul_ne_zero {M₀ : Type u_2} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a b : M₀} (ha : a ≠ 0) (hb : b ≠ 0) :

a * b ≠ 0

@[protected, instance]

def ne_zero.mul {M₀ : Type u_2} [has_zero M₀] [has_mul M₀] [no_zero_divisors M₀] {x y : M₀} [ne_zero x] [ne_zero y] :

ne_zero (x * y)

theorem eq_zero_of_zero_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] (h : 0 = 1) (a : M₀) :

a = 0

In a monoid with zero, if zero equals one, then zero is the only element.

def unique_of_zero_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] (h : 0 = 1) :

In a monoid with zero, if zero equals one, then zero is the unique element.

Somewhat arbitrarily, we define the default element to be 0. All other elements will be provably equal to it, but not necessarily definitionally equal.

Equations

unique_of_zero_eq_one h = {to_inhabited := {default := 0}, uniq := _}

theorem subsingleton_iff_zero_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] :

0 = 1 ↔ subsingleton M₀

In a monoid with zero, zero equals one if and only if all elements of that semiring are equal.

theorem subsingleton_of_zero_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] :

0 = 1 → subsingleton M₀

Alias of the forward direction of subsingleton_iff_zero_eq_one.

theorem eq_of_zero_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] (h : 0 = 1) (a b : M₀) :

a = b

theorem zero_ne_one_or_forall_eq_0 {M₀ : Type u_2} [mul_zero_one_class M₀] :

0 ≠ 1 ∨ ∀ (a : M₀), a = 0

In a monoid with zero, either zero and one are nonequal, or zero is the only element.

theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] [nontrivial M₀] {a b : M₀} (h : a * b = 1) :

a ≠ 0

theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] [nontrivial M₀] {a b : M₀} (h : a * b = 1) :

b ≠ 0

@[protected, instance]

def cancel_monoid_with_zero.to_no_zero_divisors {M₀ : Type u_2} [cancel_monoid_with_zero M₀] :

no_zero_divisors M₀

theorem mul_left_inj' {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b c : M₀} (hc : c ≠ 0) :

a * c = b * c ↔ a = b

theorem mul_right_inj' {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b c : M₀} (ha : a ≠ 0) :

a * b = a * c ↔ b = c

@[simp]

theorem mul_eq_mul_right_iff {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b c : M₀} :

a * c = b * c ↔ a = b ∨ c = 0

@[simp]

theorem mul_eq_mul_left_iff {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b c : M₀} :

a * b = a * c ↔ b = c ∨ a = 0

theorem mul_right_eq_self₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} :

a * b = a ↔ b = 1 ∨ a = 0

theorem mul_left_eq_self₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} :

a * b = b ↔ a = 1 ∨ b = 0

@[simp]

theorem mul_eq_left₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} (ha : a ≠ 0) :

a * b = a ↔ b = 1

@[simp]

theorem mul_eq_right₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} (hb : b ≠ 0) :

a * b = b ↔ a = 1

@[simp]

theorem left_eq_mul₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} (ha : a ≠ 0) :

a = a * b ↔ b = 1

@[simp]

theorem right_eq_mul₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} (hb : b ≠ 0) :

b = a * b ↔ a = 1

theorem eq_zero_of_mul_eq_self_right {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} (h₁ : b ≠ 1) (h₂ : a * b = a) :

a = 0

An element of a cancel_monoid_with_zero fixed by right multiplication by an element other than one must be zero.

theorem eq_zero_of_mul_eq_self_left {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} (h₁ : b ≠ 1) (h₂ : b * a = a) :

a = 0

An element of a cancel_monoid_with_zero fixed by left multiplication by an element other than one must be zero.

@[simp]

theorem mul_inv_cancel_right₀ {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (h : b ≠ 0) (a : G₀) :

a * b * b⁻¹ = a

@[simp]

theorem mul_inv_cancel_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) (b : G₀) :

a * (a⁻¹ * b) = b

theorem inv_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :

@[simp]

theorem inv_mul_cancel {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :

a⁻¹ * a = 1

theorem group_with_zero.mul_left_injective {G₀ : Type u_3} [group_with_zero G₀] {x : G₀} (h : x ≠ 0) :

function.injective (λ (y : G₀), x * y)

theorem group_with_zero.mul_right_injective {G₀ : Type u_3} [group_with_zero G₀] {x : G₀} (h : x ≠ 0) :

function.injective (λ (y : G₀), y * x)

@[simp]

theorem inv_mul_cancel_right₀ {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (h : b ≠ 0) (a : G₀) :

a * b⁻¹ * b = a

@[simp]

theorem inv_mul_cancel_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) (b : G₀) :

a⁻¹ * (a * b) = b

@[protected, instance]

def group_with_zero.to_division_monoid {G₀ : Type u_3} [group_with_zero G₀] :

division_monoid G₀

Equations

group_with_zero.to_division_monoid = {mul := group_with_zero.mul _inst_1, mul_assoc := _, one := group_with_zero.one _inst_1, one_mul := _, mul_one := _, npow := group_with_zero.npow _inst_1, npow_zero' := _, npow_succ' := _, inv := has_inv.inv (div_inv_monoid.to_has_inv G₀), div := group_with_zero.div _inst_1, div_eq_mul_inv := _, zpow := group_with_zero.zpow _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}

@[protected, instance]

def group_with_zero.to_cancel_monoid_with_zero {G₀ : Type u_3} [group_with_zero G₀] :

cancel_monoid_with_zero G₀

Equations

group_with_zero.to_cancel_monoid_with_zero = {mul := group_with_zero.mul _inst_1, mul_assoc := _, one := group_with_zero.one _inst_1, one_mul := _, mul_one := _, npow := group_with_zero.npow _inst_1, npow_zero' := _, npow_succ' := _, zero := group_with_zero.zero _inst_1, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}

@[simp]

theorem zero_div {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

0 / a = 0

@[simp]

theorem div_zero {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a / 0 = 0

@[simp]

theorem mul_self_mul_inv {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a * a * a⁻¹ = a

Multiplying a by itself and then by its inverse results in a (whether or not a is zero).

@[simp]

theorem mul_inv_mul_self {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a * a⁻¹ * a = a

Multiplying a by its inverse and then by itself results in a (whether or not a is zero).

@[simp]

theorem inv_mul_mul_self {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a⁻¹ * a * a = a

Multiplying a⁻¹ by a twice results in a (whether or not a is zero).

@[simp]

theorem mul_self_div_self {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a * a / a = a

Multiplying a by itself and then dividing by itself results in a, whether or not a is zero.

@[simp]

theorem div_self_mul_self {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a / a * a = a

Dividing a by itself and then multiplying by itself results in a, whether or not a is zero.

@[simp]

theorem div_self_mul_self' {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a / (a * a) = a⁻¹

theorem one_div_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :

1 / a ≠ 0

@[simp]

theorem inv_eq_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :

a⁻¹ = 0 ↔ a = 0

@[simp]

theorem zero_eq_inv {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :

0 = a⁻¹ ↔ 0 = a

@[simp]

theorem div_div_self {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :

a / (a / a) = a

Dividing a by the result of dividing a by itself results in a (whether or not a is zero).

theorem ne_zero_of_one_div_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : 1 / a ≠ 0) :

a ≠ 0

theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : 1 / a = 0) :

a = 0

theorem mul_left_surjective₀ {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :

function.surjective (λ (g : G₀), a * g)

theorem mul_right_surjective₀ {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :

function.surjective (λ (g : G₀), g * a)

theorem div_mul_eq_mul_div₀ {G₀ : Type u_3} [comm_group_with_zero G₀] (a b c : G₀) :

a / c * b = a * b / c

Order dual #

@[protected, instance]

def order_dual.mul_zero_class {α : Type u_1} [h : mul_zero_class α] :

mul_zero_class αᵒᵈ

Equations

order_dual.mul_zero_class = h

@[protected, instance]

def order_dual.mul_zero_one_class {α : Type u_1} [h : mul_zero_one_class α] :

mul_zero_one_class αᵒᵈ

Equations

order_dual.mul_zero_one_class = h

@[protected, instance]

def order_dual.no_zero_divisors {α : Type u_1} [has_mul α] [has_zero α] [h : no_zero_divisors α] :

no_zero_divisors αᵒᵈ

@[protected, instance]

def order_dual.semigroup_with_zero {α : Type u_1} [h : semigroup_with_zero α] :

semigroup_with_zero αᵒᵈ

Equations

order_dual.semigroup_with_zero = h

@[protected, instance]

def order_dual.monoid_with_zero {α : Type u_1} [h : monoid_with_zero α] :

monoid_with_zero αᵒᵈ

Equations

order_dual.monoid_with_zero = h

@[protected, instance]

def order_dual.cancel_monoid_with_zero {α : Type u_1} [h : cancel_monoid_with_zero α] :

cancel_monoid_with_zero αᵒᵈ

Equations

order_dual.cancel_monoid_with_zero = h

@[protected, instance]

def order_dual.comm_monoid_with_zero {α : Type u_1} [h : comm_monoid_with_zero α] :

comm_monoid_with_zero αᵒᵈ

Equations

order_dual.comm_monoid_with_zero = h

@[protected, instance]

def order_dual.cancel_comm_monoid_with_zero {α : Type u_1} [h : cancel_comm_monoid_with_zero α] :

cancel_comm_monoid_with_zero αᵒᵈ

Equations

order_dual.cancel_comm_monoid_with_zero = h

@[protected, instance]

def order_dual.group_with_zero {α : Type u_1} [h : group_with_zero α] :

group_with_zero αᵒᵈ

Equations

order_dual.group_with_zero = h

@[protected, instance]

def order_dual.comm_group_with_zero {α : Type u_1} [h : comm_group_with_zero α] :

comm_group_with_zero αᵒᵈ

Equations

order_dual.comm_group_with_zero = h

Lexicographic order #

@[protected, instance]

def lex.mul_zero_class {α : Type u_1} [h : mul_zero_class α] :

mul_zero_class (lex α)

Equations

lex.mul_zero_class = h

@[protected, instance]

def lex.mul_zero_one_class {α : Type u_1} [h : mul_zero_one_class α] :

mul_zero_one_class (lex α)

Equations

lex.mul_zero_one_class = h

@[protected, instance]

def lex.no_zero_divisors {α : Type u_1} [has_mul α] [has_zero α] [h : no_zero_divisors α] :

no_zero_divisors (lex α)

@[protected, instance]

def lex.semigroup_with_zero {α : Type u_1} [h : semigroup_with_zero α] :

semigroup_with_zero (lex α)

Equations

lex.semigroup_with_zero = h

@[protected, instance]

def lex.monoid_with_zero {α : Type u_1} [h : monoid_with_zero α] :

monoid_with_zero (lex α)

Equations

lex.monoid_with_zero = h

@[protected, instance]

def lex.cancel_monoid_with_zero {α : Type u_1} [h : cancel_monoid_with_zero α] :

cancel_monoid_with_zero (lex α)

Equations

lex.cancel_monoid_with_zero = h

@[protected, instance]

def lex.comm_monoid_with_zero {α : Type u_1} [h : comm_monoid_with_zero α] :

comm_monoid_with_zero (lex α)

Equations

lex.comm_monoid_with_zero = h

@[protected, instance]

def lex.cancel_comm_monoid_with_zero {α : Type u_1} [h : cancel_comm_monoid_with_zero α] :

cancel_comm_monoid_with_zero (lex α)

Equations

lex.cancel_comm_monoid_with_zero = h

@[protected, instance]

def lex.group_with_zero {α : Type u_1} [h : group_with_zero α] :

group_with_zero (lex α)

Equations

lex.group_with_zero = h

@[protected, instance]

def lex.comm_group_with_zero {α : Type u_1} [h : comm_group_with_zero α] :

comm_group_with_zero (lex α)

Equations

lex.comm_group_with_zero = h