Mathlib.Algebra.GroupWithZero.Defs

class MulZeroClass (M₀ : Type u) extends Mul , Zero :

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

mul : M₀ → M₀ → M₀
zero : M₀
zero_mul : ∀ (a : M₀), 0 * a = 0
Zero is a left absorbing element for multiplication
mul_zero : ∀ (a : M₀), a * 0 = 0
Zero is a right absorbing element for multiplication

Instances

source

@[simp]

theorem MulZeroClass.zero_mul {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀) :

0 * a = 0

Zero is a left absorbing element for multiplication

source

@[simp]

theorem MulZeroClass.mul_zero {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀) :

a * 0 = 0

Zero is a right absorbing element for multiplication

source

class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] :

Prop

A mixin for left cancellative multiplication by nonzero elements.

mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
Multiplication by a nonzero element is left cancellative.

Instances

source

theorem IsLeftCancelMulZero.mul_left_cancel_of_ne_zero {M₀ : Type u} :

∀ {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsLeftCancelMulZero M₀] {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c

Multiplication by a nonzero element is left cancellative.

source

theorem mul_left_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsLeftCancelMulZero M₀] {a : M₀} {b : M₀} {c : M₀} (ha : a ≠ 0) (h : a * b = a * c) :

b = c

source

theorem mul_right_injective₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsLeftCancelMulZero M₀] {a : M₀} (ha : a ≠ 0) :

Function.Injective fun (x : M₀) => a * x

source

class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] :

Prop

A mixin for right cancellative multiplication by nonzero elements.

mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c
Multiplicatin by a nonzero element is right cancellative.

Instances

source

theorem IsRightCancelMulZero.mul_right_cancel_of_ne_zero {M₀ : Type u} :

∀ {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsRightCancelMulZero M₀] {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c

Multiplicatin by a nonzero element is right cancellative.

source

theorem mul_right_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsRightCancelMulZero M₀] {a : M₀} {b : M₀} {c : M₀} (hb : b ≠ 0) (h : a * b = c * b) :

a = c

source

theorem mul_left_injective₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsRightCancelMulZero M₀] {b : M₀} (hb : b ≠ 0) :

Function.Injective fun (a : M₀) => a * b

source

class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] extends IsLeftCancelMulZero , IsRightCancelMulZero :

Prop

A mixin for cancellative multiplication by nonzero elements.

Instances

source

class NoZeroDivisors (M₀ : Type u_2) [Mul M₀] [Zero M₀] :

Prop

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

eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0
For all a and b of G₀, a * b = 0 implies a = 0 or b = 0.

Instances

source

theorem NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero {M₀ : Type u_2} :

∀ {inst : Mul M₀} {inst_1 : Zero M₀} [self : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0

For all a and b of G₀, a * b = 0 implies a = 0 or b = 0.

source

class SemigroupWithZero (S₀ : Type u) extends Semigroup , MulZeroClass , Mul , Zero :

Type u

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

Instances

source

class MulZeroOneClass (M₀ : Type u) extends MulOneClass , MulZeroClass , One , Mul , Zero :

Type u

A typeclass for non-associative monoids with zero elements.

Instances

source

class MonoidWithZero (M₀ : Type u) extends Monoid , MulZeroOneClass , SemigroupWithZero , Semigroup , MulOneClass , MulZeroClass , One , Mul , Zero :

Type u

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

class CancelMonoidWithZero (M₀ : Type u_2) extends MonoidWithZero , IsCancelMulZero , Monoid , MulZeroOneClass , SemigroupWithZero , Semigroup , MulOneClass , MulZeroClass , One , Mul , Zero , IsLeftCancelMulZero , IsRightCancelMulZero :

Type u_2

A type M is a CancelMonoidWithZero 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

class CommMonoidWithZero (M₀ : Type u_2) extends CommMonoid , MonoidWithZero , Monoid , CommSemigroup , MulZeroOneClass , SemigroupWithZero , Semigroup , MulOneClass , MulZeroClass , One , CommMagma , Mul , Zero :

Type u_2

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

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

a * c = b * c ↔ a = b

source

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

a * b = a * c ↔ b = c

source

theorem IsLeftCancelMulZero.to_isRightCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsLeftCancelMulZero M₀] :

IsRightCancelMulZero M₀

source

theorem IsRightCancelMulZero.to_isLeftCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsRightCancelMulZero M₀] :

IsLeftCancelMulZero M₀

source

theorem IsLeftCancelMulZero.to_isCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsLeftCancelMulZero M₀] :

IsCancelMulZero M₀

source

theorem IsRightCancelMulZero.to_isCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsRightCancelMulZero M₀] :

IsCancelMulZero M₀

source

class CancelCommMonoidWithZero (M₀ : Type u_2) extends CommMonoidWithZero , IsLeftCancelMulZero , CommMonoid , MonoidWithZero , Monoid , CommSemigroup , MulZeroOneClass , SemigroupWithZero , Semigroup , MulOneClass , MulZeroClass , One , CommMagma , Mul , Zero :

Type u_2

A type M is a CancelCommMonoidWithZero 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 100]

instance CancelCommMonoidWithZero.toCancelMonoidWithZero {M₀ : Type u_1} [CancelCommMonoidWithZero M₀] :

CancelMonoidWithZero M₀

Equations

CancelCommMonoidWithZero.toCancelMonoidWithZero = CancelMonoidWithZero.mk

source

class MulDivCancelClass (M₀ : Type u_2) [MonoidWithZero M₀] [Div M₀] :

Prop

Prop-valued mixin for a monoid with zero to be equipped with a cancelling division.

The obvious use case is groups with zero, but this condition is also satisfied by ℕ, ℤ and, more generally, any euclidean domain.

mul_div_cancel : ∀ (a b : M₀), b ≠ 0 → a * b / b = a

Instances

source

theorem MulDivCancelClass.mul_div_cancel {M₀ : Type u_2} :

∀ {inst : MonoidWithZero M₀} {inst_1 : Div M₀} [self : MulDivCancelClass M₀] (a b : M₀), b ≠ 0 → a * b / b = a

source

@[simp]

theorem mul_div_cancel_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] (a : M₀) {b : M₀} (hb : b ≠ 0) :

a * b / b = a

source

@[simp]

theorem mul_div_cancel_left₀ {M₀ : Type u_1} [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] (b : M₀) {a : M₀} (ha : a ≠ 0) :

a * b / a = b

source

class GroupWithZero (G₀ : Type u) extends MonoidWithZero , DivInvMonoid , Nontrivial , Monoid , MulZeroOneClass , SemigroupWithZero , Inv , Div , Semigroup , MulOneClass , MulZeroClass , One , Mul , Zero :

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

source

theorem GroupWithZero.inv_zero {G₀ : Type u} [self : GroupWithZero G₀] :

0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

source

theorem GroupWithZero.mul_inv_cancel {G₀ : Type u} [self : GroupWithZero G₀] (a : G₀) :

a ≠ 0 → a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

source

@[simp]

theorem inv_zero {G₀ : Type u} [GroupWithZero G₀] :

0⁻¹ = 0

source

@[simp]

theorem mul_inv_cancel₀ {G₀ : Type u} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) :

a * a⁻¹ = 1

source

@[instance 100]

instance GroupWithZero.toMulDivCancelClass {G₀ : Type u} [GroupWithZero G₀] :

MulDivCancelClass G₀

Equations

⋯ = ⋯

source

class CommGroupWithZero (G₀ : Type u_2) extends CommMonoidWithZero , GroupWithZero , CommMonoid , MonoidWithZero , DivInvMonoid , Nontrivial , Monoid , CommSemigroup , MulZeroOneClass , SemigroupWithZero , Inv , Div , Semigroup , MulOneClass , MulZeroClass , One , CommMagma , Mul , Zero :

Type u_2

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

theorem eq_zero_or_one_of_sq_eq_self {M₀ : Type u_1} [CancelMonoidWithZero M₀] {x : M₀} (hx : x ^ 2 = x) :

x = 0 ∨ x = 1

source

@[simp]

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

a * b * b⁻¹ = a

source

@[simp]

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

a * (a⁻¹ * b) = b

source

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

a * b = 0

source

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

a * b = 0

source

@[simp]

theorem mul_eq_zero {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} {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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} {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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} {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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} {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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} {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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} :

a * a = 0 ↔ a = 0

source

theorem zero_eq_mul_self {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} :

0 = a * a ↔ a = 0

source

theorem mul_self_ne_zero {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} :

a * a ≠ 0 ↔ a ≠ 0

source

theorem zero_ne_mul_self {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} :

0 ≠ a * a ↔ a ≠ 0

Documentation

Mathlib.Algebra.GroupWithZero.Defs

Typeclasses for groups with an adjoined zero element #

Main definitions #