Documentation

Mathlib.Algebra.GroupWithZero.Units.Basic

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.

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

@[simp]
theorem Units.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ˣ) {a : M₀} :
a * u = 0 a = 0
@[simp]
theorem Units.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ˣ) {a : M₀} :
u * a = 0 a = 0
theorem IsUnit.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] {a : M₀} (ha : IsUnit a) :
a 0
theorem IsUnit.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} {b : M₀} (ha : IsUnit a) :
a * b = 0 b = 0
theorem IsUnit.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} {b : M₀} (hb : IsUnit b) :
a * b = 0 a = 0
@[simp]
theorem isUnit_zero_iff {M₀ : Type u_2} [MonoidWithZero M₀] :
IsUnit 0 0 = 1
theorem not_isUnit_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] :
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₀.

Equations
Instances For
    @[simp]
    theorem Ring.inverse_unit {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ˣ) :

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

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

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

    theorem Ring.mul_inverse_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :
    theorem Ring.inverse_mul_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :
    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
    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
    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
    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
    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
    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
    @[simp]
    theorem Ring.inverse_one (M₀ : Type u_2) [MonoidWithZero M₀] :
    @[simp]
    theorem Ring.inverse_zero (M₀ : Type u_2) [MonoidWithZero M₀] :
    theorem IsUnit.ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
    @[simp]
    theorem isUnit_ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
    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.

    Equations
    • Units.mk0 a ha = { val := a, inv := a⁻¹, val_inv := , inv_val := }
    Instances For
      @[simp]
      theorem Units.mk0_one {G₀ : Type u_3} [GroupWithZero G₀] (h : optParam (1 0) ) :
      Units.mk0 1 h = 1
      @[simp]
      theorem Units.val_mk0 {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a 0) :
      (Units.mk0 a h) = a
      @[simp]
      theorem Units.mk0_val {G₀ : Type u_3} [GroupWithZero G₀] (u : G₀ˣ) (h : u 0) :
      Units.mk0 (u) h = u
      theorem Units.mul_inv' {G₀ : Type u_3} [GroupWithZero G₀] (u : G₀ˣ) :
      u * (u)⁻¹ = 1
      theorem Units.inv_mul' {G₀ : Type u_3} [GroupWithZero G₀] (u : G₀ˣ) :
      (u)⁻¹ * u = 1
      @[simp]
      theorem Units.mk0_inj {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a 0) (hb : b 0) :
      Units.mk0 a ha = Units.mk0 b hb a = b
      theorem Units.exists0 {G₀ : Type u_3} [GroupWithZero G₀] {p : G₀ˣProp} :
      (∃ (g : G₀ˣ), p g) ∃ (g : G₀), ∃ (hg : g 0), p (Units.mk0 g hg)

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

      theorem Units.exists0' {G₀ : Type u_3} [GroupWithZero G₀] {p : (g : G₀) → g 0Prop} :
      (∃ (g : G₀), ∃ (hg : g 0), p g hg) ∃ (g : G₀ˣ), p g

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

      @[simp]
      theorem Units.exists_iff_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {x : G₀} :
      (∃ (u : G₀ˣ), u = x) x 0
      theorem GroupWithZero.eq_zero_or_unit {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) :
      a = 0 ∃ (u : G₀ˣ), a = u
      theorem IsUnit.mk0 {G₀ : Type u_3} [GroupWithZero G₀] (x : G₀) (hx : x 0) :
      theorem isUnit_iff_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} :
      IsUnit a a 0
      theorem Ne.isUnit {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} :
      a 0IsUnit a

      Alias of the reverse direction of isUnit_iff_ne_zero.

      Equations
      • =
      @[simp]
      theorem Units.mk0_mul {G₀ : Type u_3} [GroupWithZero G₀] (x : G₀) (y : G₀) (hxy : x * y 0) :
      Units.mk0 (x * y) hxy = Units.mk0 x * Units.mk0 y
      theorem div_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a 0) (hb : b 0) :
      a / b 0
      @[simp]
      theorem div_eq_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} :
      a / b = 0 a = 0 b = 0
      theorem div_ne_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} :
      a / b 0 a 0 b 0
      @[simp]
      theorem div_self {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a 0) :
      a / a = 1
      theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
      a = b * c⁻¹ a * c = b
      theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
      a = b⁻¹ * c b * a = c
      theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (ha : a 0) :
      a⁻¹ * b = c b = a * c
      theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
      a * b⁻¹ = c a = c * b
      theorem mul_inv_eq_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b 0) :
      a * b⁻¹ = 1 a = b
      theorem inv_mul_eq_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a 0) :
      a⁻¹ * b = 1 a = b
      theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b 0) :
      a * b = 1 a = b⁻¹
      theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a 0) :
      a * b = 1 a⁻¹ = b
      theorem mul_eq_of_eq_mul_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (ha : a 0) (h : a = c * b⁻¹) :
      a * b = c

      A variant of eq_mul_inv_iff_mul_eq₀ that moves the nonzero hypothesis to another variable.

      theorem mul_eq_of_eq_inv_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) (h : b = a⁻¹ * c) :
      a * b = c

      A variant of eq_inv_mul_iff_mul_eq₀ that moves the nonzero hypothesis to another variable.

      theorem eq_mul_of_inv_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) (h : b⁻¹ * a = c) :
      a = b * c

      A variant of inv_mul_eq_iff_eq_mul₀ that moves the nonzero hypothesis to another variable.

      theorem eq_mul_of_mul_inv_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) (h : a * c⁻¹ = b) :
      a = b * c

      A variant of mul_inv_eq_iff_eq_mul₀ that moves the nonzero hypothesis to another variable.

      @[simp]
      theorem div_mul_cancel₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (h : b 0) :
      a / b * b = a
      @[simp]
      theorem mul_div_cancel_right₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (h : b 0) :
      a * b / b = a
      theorem mul_one_div_cancel {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a 0) :
      a * (1 / a) = 1
      theorem one_div_mul_cancel {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a 0) :
      1 / a * a = 1
      theorem div_left_inj' {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
      a / c = b / c a = b
      theorem div_eq_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
      a / b = c a = c * b
      theorem eq_div_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
      c = a / b c * b = a
      theorem div_eq_iff_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
      a / b = c c * b = a
      theorem eq_div_iff_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
      a = b / c a * c = b
      theorem div_eq_of_eq_mul {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
      a = c * ba / b = c
      theorem eq_div_of_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
      a * c = ba = b / c
      theorem div_eq_one_iff_eq {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b 0) :
      a / b = 1 a = b
      theorem div_mul_cancel_right₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (hb : b 0) (a : G₀) :
      b / (a * b) = a⁻¹
      @[deprecated div_mul_cancel_right₀]
      theorem div_mul_left {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b 0) :
      b / (a * b) = 1 / a
      theorem mul_div_mul_right {G₀ : Type u_3} [GroupWithZero G₀] {c : G₀} (a : G₀) (b : G₀) (hc : c 0) :
      a * c / (b * c) = a / b
      theorem mul_mul_div {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (hb : b 0) :
      a = a * b * (1 / b)
      theorem div_div_div_cancel_right {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} {c : G₀} (a : G₀) (hc : c 0) :
      a / c / (b / c) = a / b
      theorem div_mul_div_cancel {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} {c : G₀} (a : G₀) (hc : c 0) :
      a / c * (c / b) = a / b
      theorem div_mul_cancel_of_imp {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : b = 0a = 0) :
      a / b * b = a
      theorem mul_div_cancel_of_imp {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : b = 0a = 0) :
      a * b / b = a
      @[simp]
      theorem divp_mk0 {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (hb : b 0) :
      a /ₚ Units.mk0 b hb = a / b
      theorem Ring.inverse_eq_inv {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) :
      @[simp]
      theorem Ring.inverse_eq_inv' {G₀ : Type u_3} [GroupWithZero G₀] :
      Ring.inverse = Inv.inv
      Equations
      • CommGroupWithZero.toCancelCommMonoidWithZero = let __src := GroupWithZero.toCancelMonoidWithZero; let __src_1 := CommGroupWithZero.toCommMonoidWithZero; CancelCommMonoidWithZero.mk
      Equations
      • CommGroupWithZero.toDivisionCommMonoid = let __spread.0 := inst; let __spread.1 := GroupWithZero.toDivisionMonoid; DivisionCommMonoid.mk
      theorem div_mul_cancel_left₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (ha : a 0) (b : G₀) :
      a / (a * b) = b⁻¹
      @[deprecated div_mul_cancel_left₀]
      theorem div_mul_right {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (b : G₀) (ha : a 0) :
      a / (a * b) = 1 / b
      theorem mul_div_cancel_left_of_imp {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} {b : G₀} (h : a = 0b = 0) :
      a * b / a = b
      theorem mul_div_cancel_left₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (b : G₀) (ha : a 0) :
      a * b / a = b
      theorem mul_div_cancel_of_imp' {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} {b : G₀} (h : b = 0a = 0) :
      b * (a / b) = a
      theorem mul_div_cancel₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {b : G₀} (a : G₀) (hb : b 0) :
      b * (a / b) = a
      theorem mul_div_mul_left {G₀ : Type u_3} [CommGroupWithZero G₀] {c : G₀} (a : G₀) (b : G₀) (hc : c 0) :
      c * a / (c * b) = a / b
      theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_3} [CommGroupWithZero G₀] {b : G₀} {d : G₀} (a : G₀) (c : G₀) (hb : b 0) (hd : d 0) (h : a / b = c / d) :
      a * d = c * b
      theorem div_eq_div_iff {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} {d : G₀} (hb : b 0) (hd : d 0) :
      a / b = c / d a * d = c * b
      theorem div_eq_div_iff_div_eq_div' {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} {d : G₀} (hb : b 0) (hc : c 0) :
      a / b = c / d a / c = b / d

      The CommGroupWithZero version of div_eq_div_iff_div_eq_div.

      theorem div_div_cancel' {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} {b : G₀} (ha : a 0) :
      a / (a / b) = b
      theorem div_div_cancel_left' {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} {b : G₀} (ha : a 0) :
      a / b / a = b⁻¹
      theorem div_helper {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (b : G₀) (h : a 0) :
      1 / (a * b) * a = 1 / b
      theorem div_div_div_cancel_left' {G₀ : Type u_3} [CommGroupWithZero G₀] {c : G₀} (a : G₀) (b : G₀) (hc : c 0) :
      c / a / (c / b) = b / a
      noncomputable def groupWithZeroOfIsUnitOrEqZero {M : Type u_8} [Nontrivial M] [hM : MonoidWithZero M] (h : ∀ (a : M), IsUnit a a = 0) :

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

      Equations
      Instances For
        noncomputable def commGroupWithZeroOfIsUnitOrEqZero {M : Type u_8} [Nontrivial M] [hM : CommMonoidWithZero M] (h : ∀ (a : M), IsUnit a a = 0) :

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

        Equations
        Instances For
          @[deprecated mul_div_cancel₀]
          theorem mul_div_cancel' {G₀ : Type u_3} [CommGroupWithZero G₀] {b : G₀} (a : G₀) (hb : b 0) :
          b * (a / b) = a

          Alias of mul_div_cancel₀.