algebra.group_with_zero.defs

mul : M₀ → M₀ → M₀
mul_assoc : ∀ (a b c : M₀), a * b * c = a * (b * c)
one : M₀
one_mul : ∀ (a : M₀), 1 * a = a
mul_one : ∀ (a : M₀), a * 1 = a
npow : ℕ → M₀ → M₀
npow_zero' : (∀ (x : M₀), monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M₀), monoid_with_zero.npow n.succ x = x * monoid_with_zero.npow n x) . "try_refl_tac"
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 of this typeclass

Instances of other typeclasses for monoid_with_zero

monoid_with_zero.has_sizeof_inst

source

@[protected, instance]

def monoid_with_zero.to_semigroup_with_zero (M₀ : Type u_1) [monoid_with_zero M₀] :

semigroup_with_zero M₀

Equations

monoid_with_zero.to_semigroup_with_zero M₀ = {mul := monoid_with_zero.mul _inst_1, mul_assoc := _, zero := monoid_with_zero.zero _inst_1, zero_mul := _, mul_zero := _}

source

@[instance]

def cancel_monoid_with_zero.to_monoid_with_zero (M₀ : Type u_4) [self : 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 : M₀), a * b * c = a * (b * c)
one : M₀
one_mul : ∀ (a : M₀), 1 * a = a
mul_one : ∀ (a : M₀), a * 1 = a
npow : ℕ → M₀ → M₀
npow_zero' : (∀ (x : M₀), cancel_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M₀), cancel_monoid_with_zero.npow n.succ x = x * cancel_monoid_with_zero.npow n x) . "try_refl_tac"
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 : 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 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

source

@[protected, instance]

def cancel_monoid_with_zero.to_is_cancel_mul_zero {M₀ : Type u_1} [cancel_monoid_with_zero M₀] :

is_cancel_mul_zero M₀

A cancel_monoid_with_zero satisfies is_cancel_mul_zero.

source

@[instance]

def comm_monoid_with_zero.to_comm_monoid (M₀ : Type u_4) [self : comm_monoid_with_zero M₀] :

comm_monoid M₀

source

@[instance]

def comm_monoid_with_zero.to_monoid_with_zero (M₀ : Type u_4) [self : 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 : M₀), a * b * c = a * (b * c)
one : M₀
one_mul : ∀ (a : M₀), 1 * a = a
mul_one : ∀ (a : M₀), a * 1 = a
npow : ℕ → M₀ → M₀
npow_zero' : (∀ (x : M₀), comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M₀), comm_monoid_with_zero.npow n.succ x = x * comm_monoid_with_zero.npow n x) . "try_refl_tac"
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 of this typeclass

Instances of other typeclasses for comm_monoid_with_zero

comm_monoid_with_zero.has_sizeof_inst

source

@[class]

structure cancel_comm_monoid_with_zero (M₀ : Type u_4) :

Type u_4

mul : M₀ → M₀ → M₀
mul_assoc : ∀ (a b c : M₀), a * b * c = a * (b * c)
one : M₀
one_mul : ∀ (a : M₀), 1 * a = a
mul_one : ∀ (a : M₀), a * 1 = a
npow : ℕ → M₀ → M₀
npow_zero' : (∀ (x : M₀), cancel_comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M₀), cancel_comm_monoid_with_zero.npow n.succ x = x * cancel_comm_monoid_with_zero.npow n x) . "try_refl_tac"
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 : M₀}, a ≠ 0 → a * b = a * c → b = c

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

source

@[instance]

def cancel_comm_monoid_with_zero.to_comm_monoid_with_zero (M₀ : Type u_4) [self : cancel_comm_monoid_with_zero M₀] :

comm_monoid_with_zero M₀

source

@[protected, instance]

def cancel_comm_monoid_with_zero.to_cancel_monoid_with_zero {M₀ : Type u_1} [h : cancel_comm_monoid_with_zero M₀] :

cancel_monoid_with_zero M₀

Equations

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

source

@[instance]

def group_with_zero.to_nontrivial (G₀ : Type u) [self : group_with_zero G₀] :

nontrivial G₀

source

@[instance]

def group_with_zero.to_monoid_with_zero (G₀ : Type u) [self : 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 : G₀), a * b * c = a * (b * c)
one : G₀
one_mul : ∀ (a : G₀), 1 * a = a
mul_one : ∀ (a : G₀), a * 1 = a
npow : ℕ → G₀ → G₀
npow_zero' : (∀ (x : G₀), group_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G₀), group_with_zero.npow n.succ x = x * group_with_zero.npow n x) . "try_refl_tac"
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"
zpow : ℤ → G₀ → G₀
zpow_zero' : (∀ (a : G₀), group_with_zero.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G₀), group_with_zero.zpow (int.of_nat n.succ) a = a * group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G₀), group_with_zero.zpow -[1+ n] a = (group_with_zero.zpow ↑(n.succ) a)⁻¹) . "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 of this typeclass

Instances of other typeclasses for group_with_zero

group_with_zero.has_sizeof_inst

source

@[instance]

def group_with_zero.to_div_inv_monoid (G₀ : Type u) [self : 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 : G₀), a * b * c = a * (b * c)
one : G₀
one_mul : ∀ (a : G₀), 1 * a = a
mul_one : ∀ (a : G₀), a * 1 = a
npow : ℕ → G₀ → G₀
npow_zero' : (∀ (x : G₀), comm_group_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G₀), comm_group_with_zero.npow n.succ x = x * comm_group_with_zero.npow n x) . "try_refl_tac"
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"
zpow : ℤ → G₀ → G₀
zpow_zero' : (∀ (a : G₀), comm_group_with_zero.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G₀), comm_group_with_zero.zpow (int.of_nat n.succ) a = a * comm_group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G₀), comm_group_with_zero.zpow -[1+ n] a = (comm_group_with_zero.zpow ↑(n.succ) a)⁻¹) . "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 of this typeclass

Instances of other typeclasses for comm_group_with_zero

comm_group_with_zero.has_sizeof_inst

source

@[instance]

def comm_group_with_zero.to_group_with_zero (G₀ : Type u_4) [self : 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) [self : comm_group_with_zero G₀] :

comm_monoid_with_zero G₀

source

@[protected, instance]

def ne_zero.one (M₀ : Type u_1) [mul_zero_one_class M₀] [nontrivial M₀] :

ne_zero 1

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

source

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) :

nontrivial M₀'

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

source

theorem mul_eq_zero_of_left {M₀ : Type u_1} [mul_zero_class M₀] {a : M₀} (h : a = 0) (b : M₀) :

a * b = 0

source

theorem mul_eq_zero_of_right {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) {b : M₀} (h : b = 0) :

a * b = 0

source

@[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.

source

@[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.

source

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.

source

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.

source

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.

source

theorem mul_self_eq_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :

a * a = 0 ↔ a = 0

source

theorem zero_eq_mul_self {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :

0 = a * a ↔ a = 0

source

theorem mul_self_ne_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :

a * a ≠ 0 ↔ a ≠ 0

source

theorem zero_ne_mul_self {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :

0 ≠ a * a ↔ a ≠ 0

mathlib documentation

Typeclasses for groups with an adjoined zero element #

Main definitions #