mathlib docs: algebra.group_with

source

@[instance]

def mul_zero_class.to_has_mul (M₀ : Type u_5) [s : mul_zero_class M₀] :

has_mul M₀

source

@[class]

structure mul_zero_class :

Type u_5 → Type u_5

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_5) [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

def function.injective.mul_zero_class {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_class M₀] [has_mul M₀'] [has_zero M₀'] (f : M₀' → M₀) :

function.injective f → f 0 = 0 → (∀ (a b : M₀'), f (a * b) = f a * f b) → mul_zero_class M₀'

Pullback a mul_zero_class instance along an injective function.

Equations

function.injective.mul_zero_class f hf zero mul = {mul := has_mul.mul _inst_2, zero := 0, zero_mul := _, mul_zero := _}

source

def function.surjective.mul_zero_class {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_class M₀] [has_mul M₀'] [has_zero M₀'] (f : M₀ → M₀') :

function.surjective f → f 0 = 0 → (∀ (a b : M₀), f (a * b) = f a * f b) → mul_zero_class M₀'

Pushforward a mul_zero_class instance along an surjective function.

Equations

function.surjective.mul_zero_class f hf zero mul = {mul := has_mul.mul _inst_2, zero := 0, zero_mul := _, mul_zero := _}

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₀] {b : M₀} (a : M₀) :

b = 0 → a * b = 0

source

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

a * b ≠ 0 → a ≠ 0

source

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

a * b ≠ 0 → b ≠ 0

source

theorem ne_zero_and_ne_zero_of_mul {M₀ : Type u_1} [mul_zero_class M₀] {a b : M₀} :

a * b ≠ 0 → a ≠ 0 ∧ b ≠ 0

source

@[class]

structure no_zero_divisors (M₀ : Type u_5) [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

theorem function.injective.no_zero_divisors {M₀ : Type u_1} {M₀' : Type u_3} [has_mul M₀] [has_zero M₀] [has_mul M₀'] [has_zero M₀'] [no_zero_divisors M₀'] (f : M₀ → M₀') :

function.injective f → f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → no_zero_divisors M₀

Pushforward a no_zero_divisors instance along an injective function.

source

theorem eq_zero_of_mul_self_eq_zero {M₀ : Type u_1} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a : M₀} :

a * a = 0 → a = 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_ne_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :

a ≠ 0 → b ≠ 0 → a * b ≠ 0

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

@[instance]

def monoid_with_zero.to_monoid (M₀ : Type u_5) [s : monoid_with_zero M₀] :

monoid M₀

source

@[instance]

def monoid_with_zero.to_mul_zero_class (M₀ : Type u_5) [s : monoid_with_zero M₀] :

mul_zero_class M₀

source

@[class]

structure monoid_with_zero :

Type u_5 → Type u_5

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_5) [s : cancel_monoid_with_zero M₀] :

monoid_with_zero M₀

source

@[class]

structure cancel_monoid_with_zero :

Type u_5 → Type u_5

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

@[simp]

theorem zero_ne_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] :

0 ≠ 1

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

source

@[simp]

theorem one_ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] :

1 ≠ 0

source

theorem ne_zero_of_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a : M₀} :

a = 1 → a ≠ 0

source

theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a b : M₀} :

a * b = 1 → a ≠ 0

source

theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a b : M₀} :

a * b = 1 → b ≠ 0

source

theorem pullback_nonzero {M₀ : Type u_1} {M₀' : Type u_3} [monoid_with_zero M₀] [nontrivial M₀] [has_zero M₀'] [has_one M₀'] (f : M₀' → M₀) :

f 0 = 0 → f 1 = 1 → nontrivial M₀'

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

source

@[instance]

def comm_monoid_with_zero.to_monoid_with_zero (M₀ : Type u_5) [s : comm_monoid_with_zero M₀] :

monoid_with_zero M₀

source

@[instance]

def comm_monoid_with_zero.to_comm_monoid (M₀ : Type u_5) [s : comm_monoid_with_zero M₀] :

comm_monoid M₀

source

@[class]

structure comm_monoid_with_zero :

Type u_5 → Type u_5

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_5) [s : comm_cancel_monoid_with_zero M₀] :

cancel_monoid_with_zero M₀

source

@[class]

structure comm_cancel_monoid_with_zero :

Type u_5 → Type u_5

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 comm_cancel_monoid_with_zero.to_comm_monoid_with_zero (M₀ : Type u_5) [s : comm_cancel_monoid_with_zero M₀] :

comm_monoid_with_zero M₀

source

@[instance]

def group_with_zero.to_monoid_with_zero (G₀ : Type u_5) [s : group_with_zero G₀] :

monoid_with_zero G₀

source

@[instance]

def group_with_zero.to_has_inv (G₀ : Type u_5) [s : group_with_zero G₀] :

has_inv G₀

source

@[class]

structure group_with_zero :

Type u_5 → Type u_5

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₀
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_nontrivial (G₀ : Type u_5) [s : group_with_zero G₀] :

nontrivial G₀

source

@[instance]

def comm_group_with_zero.to_comm_monoid_with_zero (G₀ : Type u_5) [s : comm_group_with_zero G₀] :

comm_monoid_with_zero G₀

source

@[instance]

def comm_group_with_zero.to_group_with_zero (G₀ : Type u_5) [s : comm_group_with_zero G₀] :

group_with_zero G₀

source

@[class]

structure comm_group_with_zero :

Type u_5 → Type u_5

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₀
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 group_with_zero.has_div {G₀ : Type u_1} [group_with_zero G₀] :

has_div G₀

The division operation on a group with zero element.

Equations

group_with_zero.has_div = {div := λ (g h : G₀), g * h⁻¹}

source

def function.injective.monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [monoid_with_zero M₀] (f : M₀' → M₀) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : M₀'), f (x * y) = f x * f y) → monoid_with_zero M₀'

Pullback a monoid_with_zero class along an injective function.

Equations

function.injective.monoid_with_zero f hf zero one mul = {mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}

source

def function.surjective.monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [monoid_with_zero M₀] (f : M₀ → M₀') :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : M₀), f (x * y) = f x * f y) → monoid_with_zero M₀'

Pushforward a monoid_with_zero class along a surjective function.

Equations

function.surjective.monoid_with_zero f hf zero one mul = {mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}

source

def function.injective.comm_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [comm_monoid_with_zero M₀] (f : M₀' → M₀) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : M₀'), f (x * y) = f x * f y) → comm_monoid_with_zero M₀'

Pullback a monoid_with_zero class along an injective function.

Equations

function.injective.comm_monoid_with_zero f hf zero one mul = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}

source

def function.surjective.comm_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [comm_monoid_with_zero M₀] (f : M₀ → M₀') :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : M₀), f (x * y) = f x * f y) → comm_monoid_with_zero M₀'

Pushforward a monoid_with_zero class along a surjective function.

Equations

function.surjective.comm_monoid_with_zero f hf zero one mul = {mul := comm_monoid.mul (function.surjective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.surjective.comm_monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}

source

@[simp]

theorem units.ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] (u : units M₀) :

↑u ≠ 0

An element of the unit group of a nonzero monoid with zero represented as an element of the monoid is nonzero.

source

@[simp]

theorem units.mul_left_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] (u : units M₀) {a : M₀} :

a * ↑u = 0 ↔ a = 0

source

@[simp]

theorem units.mul_right_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] (u : units M₀) {a : M₀} :

↑u * a = 0 ↔ a = 0

source

theorem is_unit.ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a : M₀} :

is_unit a → a ≠ 0

source

theorem is_unit.mul_right_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] {a b : M₀} :

is_unit a → (a * b = 0 ↔ b = 0)

source

theorem is_unit.mul_left_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] {a b : M₀} :

is_unit b → (a * b = 0 ↔ a = 0)

source

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

a = 0

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

source

def unique_of_zero_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] :

0 = 1 → unique M₀

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 := _}

source

theorem subsingleton_of_zero_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] :

0 = 1 → subsingleton M₀

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

source

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

a = b

source

@[simp]

theorem is_unit_zero_iff {M₀ : Type u_1} [monoid_with_zero M₀] :

is_unit 0 ↔ 0 = 1

source

@[simp]

theorem not_is_unit_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] :

¬is_unit 0

source

theorem zero_ne_one_or_forall_eq_0 (M₀ : Type u_1) [monoid_with_zero M₀] :

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

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

source

@[instance]

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

no_zero_divisors M₀

Equations

comm_cancel_monoid_with_zero.no_zero_divisors = _

source

theorem mul_left_cancel' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :

a ≠ 0 → a * b = a * c → b = c

source

theorem mul_right_cancel' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :

b ≠ 0 → a * b = c * b → a = c

source

theorem mul_left_inj' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :

c ≠ 0 → (a * c = b * c ↔ a = b)

source

theorem mul_right_inj' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :

a ≠ 0 → (a * b = a * c ↔ b = c)

source

def function.injective.cancel_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [cancel_monoid_with_zero M₀] [has_zero M₀'] [has_mul M₀'] [has_one M₀'] (f : M₀' → M₀) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : M₀'), f (x * y) = f x * f y) → cancel_monoid_with_zero M₀'

Pullback a monoid_with_zero class along an injective function.

Equations

function.injective.cancel_monoid_with_zero f hf zero one mul = {mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}

source

theorem eq_zero_of_mul_eq_self_right {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b : M₀} :

b ≠ 1 → 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.

source

theorem eq_zero_of_mul_eq_self_left {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b : M₀} :

b ≠ 1 → 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.

source

theorem div_eq_mul_inv {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a / b = a * b⁻¹

source

@[simp]

theorem inv_zero {G₀ : Type u_2} [group_with_zero G₀] :

0⁻¹ = 0

source

@[simp]

theorem mul_inv_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → a * a⁻¹ = 1

source

def function.injective.group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (f : G₀' → G₀) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : G₀'), f (x * y) = f x * f y) → (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) → group_with_zero G₀'

Pullback a group_with_zero class along an injective function.

Equations

function.injective.group_with_zero f hf zero one mul inv = {mul := monoid_with_zero.mul (function.injective.monoid_with_zero f hf zero one mul), mul_assoc := _, one := monoid_with_zero.one (function.injective.monoid_with_zero f hf zero one mul), one_mul := _, mul_one := _, zero := monoid_with_zero.zero (function.injective.monoid_with_zero f hf zero one mul), zero_mul := _, mul_zero := _, inv := has_inv.inv _inst_5, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

def function.surjective.group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (h01 : 0 ≠ 1) (f : G₀ → G₀') :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : G₀), f (x * y) = f x * f y) → (∀ (x : G₀), f x⁻¹ = (f x)⁻¹) → group_with_zero G₀'

Pushforward a group_with_zero class along an surjective function.

Equations

function.surjective.group_with_zero h01 f hf zero one mul inv = {mul := monoid_with_zero.mul (function.surjective.monoid_with_zero f hf zero one mul), mul_assoc := _, one := monoid_with_zero.one (function.surjective.monoid_with_zero f hf zero one mul), one_mul := _, mul_one := _, zero := monoid_with_zero.zero (function.surjective.monoid_with_zero f hf zero one mul), zero_mul := _, mul_zero := _, inv := has_inv.inv _inst_5, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

@[simp]

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

a * b * b⁻¹ = a

source

@[simp]

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

a * (a⁻¹ * b) = b

source

theorem inv_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → a⁻¹ ≠ 0

source

@[simp]

theorem inv_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → a⁻¹ * a = 1

source

@[simp]

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

a * b⁻¹ * b = a

source

@[simp]

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

a⁻¹ * (a * b) = b

source

@[simp]

theorem inv_one {G₀ : Type u_2} [group_with_zero G₀] :

1⁻¹ = 1

source

@[simp]

theorem inv_inv' {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :

a⁻¹ ⁻¹ = a

source

@[simp]

theorem mul_self_mul_inv {G₀ : Type u_2} [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).

source

@[simp]

theorem mul_inv_mul_self {G₀ : Type u_2} [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).

source

@[simp]

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

a⁻¹ * a * a = a

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

source

@[simp]

theorem mul_self_div_self {G₀ : Type u_2} [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).

source

@[simp]

theorem div_self_mul_self {G₀ : Type u_2} [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).

source

theorem inv_involutive' {G₀ : Type u_2} [group_with_zero G₀] :

function.involutive has_inv.inv

source

theorem eq_inv_of_mul_right_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a * b = 1 → b = a⁻¹

source

theorem eq_inv_of_mul_left_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a * b = 1 → a = b⁻¹

source

theorem inv_injective' {G₀ : Type u_2} [group_with_zero G₀] :

function.injective has_inv.inv

source

@[simp]

theorem inv_inj' {G₀ : Type u_2} [group_with_zero G₀] {g h : G₀} :

g⁻¹ = h⁻¹ ↔ g = h

source

theorem inv_eq_iff {G₀ : Type u_2} [group_with_zero G₀] {g h : G₀} :

g⁻¹ = h ↔ h⁻¹ = g

source

def units.mk0 {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :

a ≠ 0 → units G₀

Embed a non-zero element of a group_with_zero into the unit group. By combining this function with the operations on units, or the /ₚ operation, it is possible to write a division as a partial function with three arguments.

Equations

units.mk0 a ha = {val := a, inv := a⁻¹, val_inv := _, inv_val := _}

source

@[simp]

theorem units.coe_mk0 {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :

↑(units.mk0 a h) = a

source

@[simp]

theorem units.mk0_coe {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) (h : ↑u ≠ 0) :

units.mk0 ↑u h = u

source

@[simp]

theorem units.coe_inv' {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) :

↑u⁻¹ = (↑u)⁻¹

source

@[simp]

theorem units.mul_inv' {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) :

↑u * (↑u)⁻¹ = 1

source

@[simp]

theorem units.inv_mul' {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) :

(↑u)⁻¹ * ↑u = 1

source

@[simp]

theorem units.mk0_inj {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :

units.mk0 a ha = units.mk0 b hb ↔ a = b

source

@[simp]

theorem units.exists_iff_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} :

(∃ (u : units G₀), ↑u = x) ↔ x ≠ 0

source

theorem is_unit.mk0 {G₀ : Type u_2} [group_with_zero G₀] (x : G₀) :

x ≠ 0 → is_unit x

source

theorem is_unit_iff_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} :

is_unit x ↔ x ≠ 0

source

@[instance]

def group_with_zero.no_zero_divisors {G₀ : Type u_2} [group_with_zero G₀] :

no_zero_divisors G₀

Equations

group_with_zero.no_zero_divisors = _

source

@[instance]

def group_with_zero.cancel_monoid_with_zero {G₀ : Type u_2} [group_with_zero G₀] :

cancel_monoid_with_zero G₀

Equations

group_with_zero.cancel_monoid_with_zero = {mul := group_with_zero.mul _inst_1, mul_assoc := _, one := group_with_zero.one _inst_1, one_mul := _, mul_one := _, zero := group_with_zero.zero _inst_1, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}

source

theorem mul_inv_rev' {G₀ : Type u_2} [group_with_zero G₀] (x y : G₀) :

(x * y)⁻¹ = y⁻¹ * x⁻¹

source

@[simp]

theorem div_self {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → a / a = 1

source

@[simp]

theorem div_one {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :

a / 1 = a

source

@[simp]

theorem one_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :

1 / a = a⁻¹

source

@[simp]

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

0 / a = 0

source

@[simp]

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

a / 0 = 0

source

@[simp]

theorem div_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} :

b ≠ 0 → a / b * b = a

source

theorem div_mul_cancel_of_imp {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

(b = 0 → a = 0) → a / b * b = a

source

@[simp]

theorem mul_div_cancel {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} :

b ≠ 0 → a * b / b = a

source

theorem mul_div_cancel_of_imp {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

(b = 0 → a = 0) → a * b / b = a

source

theorem mul_div_assoc {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :

a * b / c = a * (b / c)

source

theorem div_eq_mul_one_div {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) :

a / b = a * (1 / b)

source

theorem mul_one_div_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → a * (1 / a) = 1

source

theorem one_div_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → 1 / a * a = 1

source

theorem one_div_one {G₀ : Type u_2} [group_with_zero G₀] :

1 / 1 = 1

source

theorem one_div_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :

a ≠ 0 → 1 / a ≠ 0

source

theorem eq_one_div_of_mul_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a * b = 1 → b = 1 / a

source

theorem eq_one_div_of_mul_eq_one_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

b * a = 1 → b = 1 / a

source

@[simp]

theorem one_div_div {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) :

1 / (a / b) = b / a

source

theorem one_div_one_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :

1 / (1 / a) = a

source

theorem eq_of_one_div_eq_one_div {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

1 / a = 1 / b → a = b

source

@[simp]

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

a⁻¹ = 0 ↔ a = 0

source

@[simp]

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

0 = a⁻¹ ↔ 0 = a

source

theorem one_div_mul_one_div_rev {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) :

1 / a * (1 / b) = 1 / (b * a)

source

theorem divp_eq_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) (u : units G₀) :

a /ₚ u = a / ↑u

source

@[simp]

theorem divp_mk0 {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} (hb : b ≠ 0) :

a /ₚ units.mk0 b hb = a / b

source

theorem inv_div {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

(a / b)⁻¹ = b / a

source

theorem inv_div_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a⁻¹ / b = (b * a)⁻¹

source

theorem div_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a ≠ 0 → b ≠ 0 → a / b ≠ 0

source

@[simp]

theorem div_eq_zero_iff {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a / b = 0 ↔ a = 0 ∨ b = 0

source

theorem div_ne_zero_iff {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

source

theorem div_left_inj' {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :

c ≠ 0 → (a / c = b / c ↔ a = b)

source

theorem div_eq_iff_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :

b ≠ 0 → (a / b = c ↔ c * b = a)

source

theorem eq_div_iff_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :

c ≠ 0 → (a = b / c ↔ a * c = b)

source

theorem div_eq_of_eq_mul {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} (hx : x ≠ 0) {y z : G₀} :

y = z * x → y / x = z

source

theorem eq_div_of_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} (hx : x ≠ 0) {y z : G₀} :

z * x = y → z = y / x

source

theorem eq_of_div_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

a / b = 1 → a = b

source

theorem div_eq_one_iff_eq {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

b ≠ 0 → (a / b = 1 ↔ a = b)

source

theorem div_mul_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

b ≠ 0 → b / (a * b) = 1 / a

source

theorem mul_div_mul_right {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) {c : G₀} :

c ≠ 0 → a * c / (b * c) = a / b

source

theorem mul_mul_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} :

b ≠ 0 → a = a * b * (1 / b)

source

@[instance]

def comm_group_with_zero.comm_cancel_monoid_with_zero {G₀ : Type u_2} [comm_group_with_zero G₀] :

comm_cancel_monoid_with_zero G₀

Equations

source

def function.injective.comm_group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [comm_group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (f : G₀' → G₀) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : G₀'), f (x * y) = f x * f y) → (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) → comm_group_with_zero G₀'

Pullback a comm_group_with_zero class along an injective function.

Equations

function.injective.comm_group_with_zero f hf zero one mul inv = {mul := group_with_zero.mul (function.injective.group_with_zero f hf zero one mul inv), mul_assoc := _, one := group_with_zero.one (function.injective.group_with_zero f hf zero one mul inv), one_mul := _, mul_one := _, mul_comm := _, zero := group_with_zero.zero (function.injective.group_with_zero f hf zero one mul inv), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (function.injective.group_with_zero f hf zero one mul inv), exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

def function.surjective.comm_group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [comm_group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (h01 : 0 ≠ 1) (f : G₀ → G₀') :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : G₀), f (x * y) = f x * f y) → (∀ (x : G₀), f x⁻¹ = (f x)⁻¹) → comm_group_with_zero G₀'

Pushforward a comm_group_with_zero class along an surjective function.

Equations

function.surjective.comm_group_with_zero h01 f hf zero one mul inv = {mul := group_with_zero.mul (function.surjective.group_with_zero h01 f hf zero one mul inv), mul_assoc := _, one := group_with_zero.one (function.surjective.group_with_zero h01 f hf zero one mul inv), one_mul := _, mul_one := _, mul_comm := _, zero := group_with_zero.zero (function.surjective.group_with_zero h01 f hf zero one mul inv), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (function.surjective.group_with_zero h01 f hf zero one mul inv), exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

theorem mul_inv' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :

(a * b)⁻¹ = a⁻¹ * b⁻¹

source

theorem one_div_mul_one_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b : G₀) :

1 / a * (1 / b) = 1 / (a * b)

source

theorem div_mul_right {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) :

a ≠ 0 → a / (a * b) = 1 / b

source

theorem mul_div_cancel_left_of_imp {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :

(a = 0 → b = 0) → a * b / a = b

source

theorem mul_div_cancel_left {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) :

a ≠ 0 → a * b / a = b

source

theorem mul_div_cancel_of_imp' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :

(b = 0 → a = 0) → b * (a / b) = a

source

theorem mul_div_cancel' {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b : G₀} :

b ≠ 0 → b * (a / b) = a

source

theorem div_mul_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c d : G₀) :

a / b * (c / d) = a * c / (b * d)

source

theorem mul_div_mul_left {G₀ : Type u_2} [comm_group_with_zero G₀] (a b : G₀) {c : G₀} :

c ≠ 0 → c * a / (c * b) = a / b

source

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

b / c * a = b * a / c

source

theorem div_mul_eq_mul_div_comm {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

b / c * a = b * (a / c)

source

theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b : G₀} (c : G₀) {d : G₀} :

b ≠ 0 → d ≠ 0 → a / b = c / d → a * d = c * b

source

theorem div_div_eq_mul_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a / (b / c) = a * c / b

source

theorem div_div_eq_div_mul {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a / b / c = a / (b * c)

source

theorem div_div_div_div_eq {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b c d : G₀} :

a / b / (c / d) = a * d / (b * c)

source

theorem div_mul_eq_div_mul_one_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a / (b * c) = a / b * (1 / c)

source

@[simp]

theorem div_div_self {G₀ : Type u_2} [comm_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).

source

theorem ne_zero_of_one_div_ne_zero {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} :

1 / a ≠ 0 → a ≠ 0

source

theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} :

1 / a = 0 → a = 0

source

theorem div_helper {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) :

a ≠ 0 → 1 / (a * b) * a = 1 / b

source

theorem div_eq_inv_mul {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :

a / b = b⁻¹ * a

source

theorem mul_div_right_comm {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a * b / c = a / c * b

source

theorem mul_comm_div' {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a / b * c = a * (c / b)

source

theorem div_mul_comm' {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a / b * c = c / b * a

source

theorem mul_div_comm {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :

a * (b / c) = b * (a / c)

source

theorem div_right_comm {G₀ : Type u_2} [comm_group_with_zero G₀] {b c : G₀} (a : G₀) :

a / b / c = a / c / b

source

theorem div_div_div_cancel_right {G₀ : Type u_2} [comm_group_with_zero G₀] {b c : G₀} (a : G₀) :

c ≠ 0 → a / c / (b / c) = a / b

source

theorem div_mul_div_cancel {G₀ : Type u_2} [comm_group_with_zero G₀] {b c : G₀} (a : G₀) :

c ≠ 0 → a / c * (c / b) = a / b

source

theorem div_eq_div_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {a b c d : G₀} :

b ≠ 0 → d ≠ 0 → (a / b = c / d ↔ a * d = c * b)

source

theorem div_eq_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {a b c : G₀} :

b ≠ 0 → (a / b = c ↔ a = c * b)

source

theorem eq_div_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {a b c : G₀} :

b ≠ 0 → (c = a / b ↔ c * b = a)

source

theorem div_div_cancel' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :

a ≠ 0 → a / (a / b) = b

source

@[simp]

theorem semiconj_by.zero_right {G₀ : Type u_2} [mul_zero_class G₀] (a : G₀) :

semiconj_by a 0 0

source

@[simp]

theorem semiconj_by.zero_left {G₀ : Type u_2} [mul_zero_class G₀] (x y : G₀) :

semiconj_by 0 x y

source

@[simp]

theorem semiconj_by.inv_symm_left_iff' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

semiconj_by a⁻¹ x y ↔ semiconj_by a y x

source

theorem semiconj_by.inv_symm_left' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

semiconj_by a x y → semiconj_by a⁻¹ y x

source

theorem semiconj_by.inv_right' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

semiconj_by a x y → semiconj_by a x⁻¹ y⁻¹

source

@[simp]

theorem semiconj_by.inv_right_iff' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y

source

theorem semiconj_by.div_right {G₀ : Type u_2} [group_with_zero G₀] {a x y x' y' : G₀} :

semiconj_by a x y → semiconj_by a x' y' → semiconj_by a (x / x') (y / y')

source

@[simp]

theorem commute.zero_right {G₀ : Type u_2} [mul_zero_class G₀] (a : G₀) :

commute a 0

source

@[simp]

theorem commute.zero_left {G₀ : Type u_2} [mul_zero_class G₀] (a : G₀) :

commute 0 a

source

@[simp]

theorem commute.inv_left_iff' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

commute a⁻¹ b ↔ commute a b

source

theorem commute.inv_left' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

commute a b → commute a⁻¹ b

source

@[simp]

theorem commute.inv_right_iff' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

commute a b⁻¹ ↔ commute a b

source

theorem commute.inv_right' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

commute a b → commute a b⁻¹

source

theorem commute.inv_inv' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

commute a b → commute a⁻¹ b⁻¹

source

@[simp]

theorem commute.div_right {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :

commute a b → commute a c → commute a (b / c)

source

@[simp]

theorem commute.div_left {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :

commute a c → commute b c → commute (a / b) c

source

theorem monoid_hom.map_ne_zero {M₀ : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] (f : G₀ →* M₀) (h0 : ⇑f 0 = 0) {a : G₀} :

⇑f a ≠ 0 ↔ a ≠ 0

source

theorem monoid_hom.map_eq_zero {M₀ : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] (f : G₀ →* M₀) (h0 : ⇑f 0 = 0) {a : G₀} :

⇑f a = 0 ↔ a = 0

source