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

ink

@[simp]

theorem Units.ne_zero {M₀ : Type u_1} [inst : MonoidWithZero M₀] [inst : 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

ink

@[simp]

theorem Units.mul_left_eq_zero {M₀ : Type u_1} [inst : MonoidWithZero M₀] (u : M₀ˣ) {a : M₀} :

a * ↑u = 0 ↔ a = 0

source

ink

@[simp]

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

↑u * a = 0 ↔ a = 0

source

ink

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

a ≠ 0

source

ink

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

a * b = 0 ↔ b = 0

source

ink

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

a * b = 0 ↔ a = 0

source

ink

@[simp]

theorem isUnit_zero_iff {M₀ : Type u_1} [inst : MonoidWithZero M₀] :

IsUnit 0 ↔ 0 = 1

source

ink

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

¬IsUnit 0

source

ink

noncomputable def Ring.inverse {M₀ : Type u_1} [inst : 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₀.

Equations

Ring.inverse x = if h : IsUnit x then ↑(IsUnit.unit h)⁻¹ else 0

source

ink

@[simp]

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

Ring.inverse ↑u = ↑u⁻¹

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

source

ink

@[simp]

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

Ring.inverse x = 0

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

source

ink

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

x * Ring.inverse x = 1

source

ink

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

Ring.inverse x * x = 1

source

ink

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

y * x * Ring.inverse x = y

source

ink

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

y * Ring.inverse x * x = y

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

@[simp]

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

Ring.inverse 1 = 1

source

ink

@[simp]

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

Ring.inverse 0 = 0

source

ink

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

IsUnit a → IsUnit (Ring.inverse a)

source

ink

@[simp]

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

IsUnit (Ring.inverse a) ↔ IsUnit a

source

ink

def Units.mk0 {G₀ : Type u_1} [inst : 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.

Equations

Units.mk0 a ha = { val := a, inv := a⁻¹, val_inv := (_ : a * a⁻¹ = 1), inv_val := (_ : a⁻¹ * a = 1) }

source

ink

@[simp]

theorem Units.mk0_one {G₀ : Type u_1} [inst : GroupWithZero G₀] (h : optParam (1 ≠ 0) (_ : 1 ≠ 0)) :

Units.mk0 1 h = 1

source

ink

@[simp]

theorem Units.val_mk0 {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0) :

↑(Units.mk0 a h) = a

source

ink

@[simp]

theorem Units.mk0_val {G₀ : Type u_1} [inst : GroupWithZero G₀] (u : G₀ˣ) (h : ↑u ≠ 0) :

Units.mk0 (↑u) h = u

source

ink

theorem Units.mul_inv' {G₀ : Type u_1} [inst : GroupWithZero G₀] (u : G₀ˣ) :

↑u * (↑u)⁻¹ = 1

source

ink

theorem Units.inv_mul' {G₀ : Type u_1} [inst : GroupWithZero G₀] (u : G₀ˣ) :

(↑u)⁻¹ * ↑u = 1

source

ink

@[simp]

theorem Units.mk0_inj {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :

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

source

ink

theorem Units.exists0 {G₀ : Type u_1} [inst : GroupWithZero G₀] {p : G₀ˣ → Prop} :

(∃ g, p g) ↔ ∃ g hg, p (Units.mk0 g hg)

In a group with zero, an existential over a unit can be rewritten in terms of Units.mk0.

source

ink

theorem Units.exists0' {G₀ : Type u_1} [inst : GroupWithZero G₀] {p : (g : G₀) → g ≠ 0 → Prop} :

(∃ g hg, p g hg) ↔ ∃ g, p ↑g (_ : ↑g ≠ 0)

An alternative version of Units.exists0. This one is useful if Lean cannot figure out p when using Units.exists0 from right to left.

source

ink

@[simp]

theorem Units.exists_iff_ne_zero {G₀ : Type u_1} [inst : GroupWithZero G₀] {x : G₀} :

(∃ u, ↑u = x) ↔ x ≠ 0

source

ink

theorem GroupWithZero.eq_zero_or_unit {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) :

a = 0 ∨ ∃ u, a = ↑u

source

ink

theorem IsUnit.mk0 {G₀ : Type u_1} [inst : GroupWithZero G₀] (x : G₀) (hx : x ≠ 0) :

IsUnit x

source

ink

theorem isUnit_iff_ne_zero {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} :

IsUnit a ↔ a ≠ 0

source

ink

theorem Ne.isUnit {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} :

a ≠ 0 → IsUnit a

Alias of the reverse direction of isUnit_iff_ne_zero.

source

ink

instance GroupWithZero.noZeroDivisors {G₀ : Type u_1} [inst : GroupWithZero G₀] :

NoZeroDivisors G₀

Equations

@GroupWithZero.noZeroDivisors = @GroupWithZero.noZeroDivisors.proof_1

source

ink

instance GroupWithZero.cancelMonoidWithZero {G₀ : Type u_1} [inst : GroupWithZero G₀] :

CancelMonoidWithZero G₀

Equations

GroupWithZero.cancelMonoidWithZero = let src := inst; CancelMonoidWithZero.mk

source

ink

@[simp]

theorem Units.mk0_mul {G₀ : Type u_1} [inst : GroupWithZero G₀] (x : G₀) (y : G₀) (hxy : x * y ≠ 0) :

Units.mk0 (x * y) hxy = Units.mk0 x (_ : x ≠ 0) * Units.mk0 y (_ : y ≠ 0)

source

ink

theorem div_ne_zero {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :

a / b ≠ 0

source

ink

@[simp]

theorem div_eq_zero_iff {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} :

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

source

ink

theorem div_ne_zero_iff {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} :

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

source

ink

theorem Ring.inverse_eq_inv {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) :

Ring.inverse a = a⁻¹

source

ink

@[simp]

theorem Ring.inverse_eq_inv' {G₀ : Type u_1} [inst : GroupWithZero G₀] :

Ring.inverse = Inv.inv

source

ink

instance CommGroupWithZero.cancelCommMonoidWithZero {G₀ : Type u_1} [inst : CommGroupWithZero G₀] :

CancelCommMonoidWithZero G₀

Equations

CommGroupWithZero.cancelCommMonoidWithZero = let src := GroupWithZero.cancelMonoidWithZero; let src_1 := CommGroupWithZero.toCommMonoidWithZero; CancelCommMonoidWithZero.mk

source

ink

instance CommGroupWithZero.toDivisionCommMonoid {G₀ : Type u_1} [inst : CommGroupWithZero G₀] :

DivisionCommMonoid G₀

Equations

CommGroupWithZero.toDivisionCommMonoid = let src := inst; let src := GroupWithZero.toDivisionMonoid; DivisionCommMonoid.mk (_ : ∀ (a b : G₀), a * b = b * a)

source

ink

noncomputable def groupWithZeroOfIsUnitOrEqZero {M : Type u_1} [inst : Nontrivial M] [hM : MonoidWithZero M] (h : ∀ (a : M), IsUnit a ∨ a = 0) :

GroupWithZero M

Constructs a GroupWithZero structure on a MonoidWithZero consisting only of units and 0.

Equations

One or more equations did not get rendered due to their size.

source

ink

noncomputable def commGroupWithZeroOfIsUnitOrEqZero {M : Type u_1} [inst : Nontrivial M] [hM : CommMonoidWithZero M] (h : ∀ (a : M), IsUnit a ∨ a = 0) :

CommGroupWithZero M

Constructs a CommGroupWithZero structure on a CommMonoidWithZero consisting only of units and 0.

Equations

commGroupWithZeroOfIsUnitOrEqZero h = let src := groupWithZeroOfIsUnitOrEqZero h; CommGroupWithZero.mk GroupWithZero.zpow (_ : 0⁻¹ = 0) (_ : ∀ (a : M), a ≠ 0 → a * a⁻¹ = 1)

Lemmas about units in a MonoidWithZero or a GroupWithZero. #

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