Lemmas about units in a `MonoidWithZero` or a `GroupWithZero`. #

We also define Ring.inverse, a globally defined function on any ring (in fact any MonoidWithZero), which inverts units and sends non-units to zero.

source

@[simp]

theorem Units.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] (u : 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_2} [MonoidWithZero M₀] (u : M₀ˣ) {a : M₀} :

a * ↑u = 0 ↔ a = 0

source

@[simp]

theorem Units.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ˣ) {a : M₀} :

↑u * a = 0 ↔ a = 0

source

theorem IsUnit.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] {a : M₀} (ha : IsUnit a) :

a ≠ 0

source

theorem IsUnit.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} {b : M₀} (ha : IsUnit a) :

a * b = 0 ↔ b = 0

source

theorem IsUnit.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} {b : M₀} (hb : IsUnit b) :

a * b = 0 ↔ a = 0

source

@[simp]

theorem isUnit_zero_iff {M₀ : Type u_2} [MonoidWithZero M₀] :

IsUnit 0 ↔ 0 = 1

source

theorem not_isUnit_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] :

¬IsUnit 0

source

noncomputable def Ring.inverse {M₀ : Type u_2} [MonoidWithZero M₀] :

M₀ → M₀

Introduce a function inverse on a monoid with zero M₀, which sends x to x⁻¹ if x is invertible and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Note that while this is in the Ring namespace for brevity, it requires the weaker assumption MonoidWithZero M₀ instead of Ring M₀.

Instances For

source

@[simp]

theorem Ring.inverse_unit {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ˣ) :

Ring.inverse ↑u = ↑u⁻¹

By definition, if x is invertible then inverse x = x⁻¹.

source

@[simp]

theorem Ring.inverse_non_unit {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : ¬IsUnit x) :

Ring.inverse x = 0

By definition, if x is not invertible then inverse x = 0.

source

theorem Ring.mul_inverse_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :

x * Ring.inverse x = 1

source

theorem Ring.inverse_mul_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :

Ring.inverse x * x = 1

source

theorem Ring.mul_inverse_cancel_right {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (y : M₀) (h : IsUnit x) :

y * x * Ring.inverse x = y

source

theorem Ring.inverse_mul_cancel_right {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (y : M₀) (h : IsUnit x) :

y * Ring.inverse x * x = y

source

theorem Ring.mul_inverse_cancel_left {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (y : M₀) (h : IsUnit x) :

x * (Ring.inverse x * y) = y

source

theorem Ring.inverse_mul_cancel_left {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (y : M₀) (h : IsUnit x) :

Ring.inverse x * (x * y) = y

source

theorem Ring.inverse_mul_eq_iff_eq_mul {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (y : M₀) (z : M₀) (h : IsUnit x) :

Ring.inverse x * y = z ↔ y = x * z

source

theorem Ring.eq_mul_inverse_iff_mul_eq {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (y : M₀) (z : M₀) (h : IsUnit z) :

x = y * Ring.inverse z ↔ x * z = y

source

@[simp]

theorem Ring.inverse_one (M₀ : Type u_2) [MonoidWithZero M₀] :

Ring.inverse 1 = 1

source

@[simp]

theorem Ring.inverse_zero (M₀ : Type u_2) [MonoidWithZero M₀] :

Ring.inverse 0 = 0

source

theorem IsUnit.ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :

IsUnit a → IsUnit (Ring.inverse a)

source

@[simp]

theorem isUnit_ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :

IsUnit (Ring.inverse a) ↔ IsUnit a

source

def Units.mk0 {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :

G₀ˣ

Embed a non-zero element of a GroupWithZero 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.

Instances For

source

@[simp]