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.

theorem Units.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] (u : Units M₀) : Ne u.val 0

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

theorem Units.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : Units M₀) {a : M₀} : Iff (Eq (HMul.hMul a u.val) 0) (Eq a 0)

theorem Units.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : Units M₀) {a : M₀} : Iff (Eq (HMul.hMul u.val a) 0) (Eq a 0)

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

theorem IsUnit.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a b : M₀} (ha : IsUnit a) : Iff (Eq (HMul.hMul a b) 0) (Eq b 0)

theorem IsUnit.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a b : M₀} (hb : IsUnit b) : Iff (Eq (HMul.hMul a b) 0) (Eq a 0)

theorem isUnit_zero_iff {M₀ : Type u_2} [MonoidWithZero M₀] : Iff (IsUnit 0) (Eq 0 1)

theorem not_isUnit_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] : Not (IsUnit 0)

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

• Eq (Ring.inverse x) (if h : IsUnit x then (Inv.inv h.unit).val else 0)

theorem Ring.inverse_unit {M₀ : Type u_2} [MonoidWithZero M₀] (u : Units M₀) : Eq (inverse u.val) (Inv.inv u).val

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

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

theorem Ring.inverse_of_isUnit {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} (h : IsUnit x) : Eq (inverse x) (Inv.inv h.unit).val

theorem Ring.inverse_non_unit {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : Not (IsUnit x)) : Eq (inverse x) 0

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) : Eq (HMul.hMul x (inverse x)) 1

theorem Ring.inverse_mul_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) : Eq (HMul.hMul (inverse x) x) 1

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

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

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

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

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

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

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

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

theorem IsUnit.ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} : IsUnit a → IsUnit (Ring.inverse a)

theorem isUnit_ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} : Iff (IsUnit (Ring.inverse a)) (IsUnit a)

def Units.mk0 {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) (ha : Ne a 0) : Units 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

• Eq (Units.mk0 a ha) { val := a, inv := Inv.inv a, val_inv := ⋯, inv_val := ⋯ }

theorem Units.mk0_one {G₀ : Type u_3} [GroupWithZero G₀] (h : Ne 1 0 := ⋯) : Eq (mk0 1 h) 1

theorem Units.val_mk0 {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : Ne a 0) : Eq (mk0 a h).val a

theorem Units.mk0_val {G₀ : Type u_3} [GroupWithZero G₀] (u : Units G₀) (h : Ne u.val 0) : Eq (mk0 u.val h) u

theorem Units.mul_inv' {G₀ : Type u_3} [GroupWithZero G₀] (u : Units G₀) : Eq (HMul.hMul u.val (Inv.inv u.val)) 1

theorem Units.inv_mul' {G₀ : Type u_3} [GroupWithZero G₀] (u : Units G₀) : Eq (HMul.hMul (Inv.inv u.val) u.val) 1

theorem Units.mk0_inj {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : Ne a 0) (hb : Ne b 0) : Iff (Eq (mk0 a ha) (mk0 b hb)) (Eq a b)

theorem Units.exists0 {G₀ : Type u_3} [GroupWithZero G₀] {p : Units G₀ → Prop} : Iff (Exists fun (g : Units G₀) => p g) (Exists fun (g : G₀) => Exists fun (hg : Ne g 0) => p (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₀) → Ne g 0 → Prop} : Iff (Exists fun (g : G₀) => Exists fun (hg : Ne g 0) => p g hg) (Exists fun (g : Units G₀) => p g.val ⋯)

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

theorem Units.exists_iff_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {p : G₀ → Prop} : Iff (Exists fun (u : Units G₀) => p u.val) (Exists fun (x : G₀) => And (Ne x 0) (p x))

theorem GroupWithZero.eq_zero_or_unit {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) : Or (Eq a 0) (Exists fun (u : Units G₀) => Eq a u.val)

theorem IsUnit.mk0 {G₀ : Type u_3} [GroupWithZero G₀] (x : G₀) (hx : Ne x 0) : IsUnit x

theorem isUnit_iff_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} : Iff (IsUnit a) (Ne a 0)

theorem Ne.isUnit {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} : Ne a 0 → IsUnit a

Alias of the reverse direction of isUnit_iff_ne_zero.

theorem GroupWithZero.noZeroDivisors {G₀ : Type u_3} [GroupWithZero G₀] : NoZeroDivisors G₀

theorem Units.mk0_mul {G₀ : Type u_3} [GroupWithZero G₀] (x y : G₀) (hxy : Ne (HMul.hMul x y) 0) : Eq (mk0 (HMul.hMul x y) hxy) (HMul.hMul (mk0 x ⋯) (mk0 y ⋯))

theorem div_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : Ne a 0) (hb : Ne b 0) : Ne (HDiv.hDiv a b) 0

theorem div_eq_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} : Iff (Eq (HDiv.hDiv a b) 0) (Or (Eq a 0) (Eq b 0))

theorem div_ne_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} : Iff (Ne (HDiv.hDiv a b) 0) (And (Ne a 0) (Ne b 0))

theorem div_self {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : Ne a 0) : Eq (HDiv.hDiv a a) 1

theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : Ne c 0) : Iff (Eq a (HMul.hMul b (Inv.inv c))) (Eq (HMul.hMul a c) b)

theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Iff (Eq a (HMul.hMul (Inv.inv b) c)) (Eq (HMul.hMul b a) c)

theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (ha : Ne a 0) : Iff (Eq (HMul.hMul (Inv.inv a) b) c) (Eq b (HMul.hMul a c))

theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Iff (Eq (HMul.hMul a (Inv.inv b)) c) (Eq a (HMul.hMul c b))

theorem mul_inv_eq_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (hb : Ne b 0) : Iff (Eq (HMul.hMul a (Inv.inv b)) 1) (Eq a b)

theorem inv_mul_eq_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : Ne a 0) : Iff (Eq (HMul.hMul (Inv.inv a) b) 1) (Eq a b)

theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (hb : Ne b 0) : Iff (Eq (HMul.hMul a b) 1) (Eq a (Inv.inv b))

theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : Ne a 0) : Iff (Eq (HMul.hMul a b) 1) (Eq (Inv.inv a) b)

theorem mul_eq_of_eq_mul_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (ha : Ne a 0) (h : Eq a (HMul.hMul c (Inv.inv b))) : Eq (HMul.hMul 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 b c : G₀} (hb : Ne b 0) (h : Eq b (HMul.hMul (Inv.inv a) c)) : Eq (HMul.hMul 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 b c : G₀} (hc : Ne c 0) (h : Eq (HMul.hMul (Inv.inv b) a) c) : Eq a (HMul.hMul 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 b c : G₀} (hb : Ne b 0) (h : Eq (HMul.hMul a (Inv.inv c)) b) : Eq a (HMul.hMul b c)

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

theorem div_mul_cancel₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (h : Ne b 0) : Eq (HMul.hMul (HDiv.hDiv a b) b) a

theorem mul_one_div_cancel {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : Ne a 0) : Eq (HMul.hMul a (HDiv.hDiv 1 a)) 1

theorem one_div_mul_cancel {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : Ne a 0) : Eq (HMul.hMul (HDiv.hDiv 1 a) a) 1

theorem div_left_inj' {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : Ne c 0) : Iff (Eq (HDiv.hDiv a c) (HDiv.hDiv b c)) (Eq a b)

theorem div_eq_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Iff (Eq (HDiv.hDiv a b) c) (Eq a (HMul.hMul c b))

theorem eq_div_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Iff (Eq c (HDiv.hDiv a b)) (Eq (HMul.hMul c b) a)

theorem div_eq_iff_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Iff (Eq (HDiv.hDiv a b) c) (Eq (HMul.hMul c b) a)

theorem eq_div_iff_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : Ne c 0) : Iff (Eq a (HDiv.hDiv b c)) (Eq (HMul.hMul a c) b)

theorem div_eq_of_eq_mul {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Eq a (HMul.hMul c b) → Eq (HDiv.hDiv a b) c

theorem eq_div_of_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : Ne c 0) : Eq (HMul.hMul a c) b → Eq a (HDiv.hDiv b c)

theorem div_eq_one_iff_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (hb : Ne b 0) : Iff (Eq (HDiv.hDiv a b) 1) (Eq a b)

theorem div_mul_cancel_right₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (hb : Ne b 0) (a : G₀) : Eq (HDiv.hDiv b (HMul.hMul a b)) (Inv.inv a)

theorem mul_div_mul_right {G₀ : Type u_3} [GroupWithZero G₀] {c : G₀} (a b : G₀) (hc : Ne c 0) : Eq (HDiv.hDiv (HMul.hMul a c) (HMul.hMul b c)) (HDiv.hDiv a b)

theorem mul_mul_div {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (hb : Ne b 0) : Eq a (HMul.hMul (HMul.hMul a b) (HDiv.hDiv 1 b))

theorem div_div_div_cancel_right₀ {G₀ : Type u_3} [GroupWithZero G₀] {c : G₀} (hc : Ne c 0) (a b : G₀) : Eq (HDiv.hDiv (HDiv.hDiv a c) (HDiv.hDiv b c)) (HDiv.hDiv a b)

theorem div_mul_div_cancel₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : Ne b 0) : Eq (HMul.hMul (HDiv.hDiv a b) (HDiv.hDiv b c)) (HDiv.hDiv a c)

theorem div_mul_cancel_of_imp {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (h : Eq b 0 → Eq a 0) : Eq (HMul.hMul (HDiv.hDiv a b) b) a

theorem mul_div_cancel_of_imp {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (h : Eq b 0 → Eq a 0) : Eq (HDiv.hDiv (HMul.hMul a b) b) a

theorem divp_mk0 {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (hb : Ne b 0) : Eq (divp a (Units.mk0 b hb)) (HDiv.hDiv a b)

theorem pow_sub₀ {G₀ : Type u_3} [GroupWithZero G₀] {m n : Nat} (a : G₀) (ha : Ne a 0) (h : LE.le n m) : Eq (HPow.hPow a (HSub.hSub m n)) (HMul.hMul (HPow.hPow a m) (Inv.inv (HPow.hPow a n)))

theorem pow_sub_of_lt {G₀ : Type u_3} [GroupWithZero G₀] {m n : Nat} (a : G₀) (h : LT.lt n m) : Eq (HPow.hPow a (HSub.hSub m n)) (HMul.hMul (HPow.hPow a m) (Inv.inv (HPow.hPow a n)))

theorem inv_pow_sub₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {m n : Nat} (ha : Ne a 0) (h : LE.le n m) : Eq (HPow.hPow (Inv.inv a) (HSub.hSub m n)) (HMul.hMul (Inv.inv (HPow.hPow a m)) (HPow.hPow a n))

theorem inv_pow_sub_of_lt {G₀ : Type u_3} [GroupWithZero G₀] {m n : Nat} (a : G₀) (h : LT.lt n m) : Eq (HPow.hPow (Inv.inv a) (HSub.hSub m n)) (HMul.hMul (Inv.inv (HPow.hPow a m)) (HPow.hPow a n))

theorem zpow_sub₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : Ne a 0) (m n : Int) : Eq (HPow.hPow a (HSub.hSub m n)) (HDiv.hDiv (HPow.hPow a m) (HPow.hPow a n))

theorem zpow_natCast_sub_natCast₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : Ne a 0) (m n : Nat) : Eq (HPow.hPow a (HSub.hSub m.cast n.cast)) (HDiv.hDiv (HPow.hPow a m) (HPow.hPow a n))

theorem zpow_natCast_sub_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : Ne a 0) (n : Nat) : Eq (HPow.hPow a (HSub.hSub n.cast 1)) (HDiv.hDiv (HPow.hPow a n) a)

theorem zpow_one_sub_natCast₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : Ne a 0) (n : Nat) : Eq (HPow.hPow a (HSub.hSub 1 n.cast)) (HDiv.hDiv a (HPow.hPow a n))

theorem zpow_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (n : Int) : Ne a 0 → Ne (HPow.hPow a n) 0

theorem eq_zero_of_zpow_eq_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {n : Int} : Eq (HPow.hPow a n) 0 → Eq a 0

theorem zpow_eq_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {n : Int} (hn : Ne n 0) : Iff (Eq (HPow.hPow a n) 0) (Eq a 0)

theorem zpow_ne_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {n : Int} (hn : Ne n 0) : Iff (Ne (HPow.hPow a n) 0) (Ne a 0)

theorem zpow_neg_mul_zpow_self {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (n : Int) (ha : Ne a 0) : Eq (HMul.hMul (HPow.hPow a (Neg.neg n)) (HPow.hPow a n)) 1

theorem Ring.inverse_eq_inv {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) : Eq (inverse a) (Inv.inv a)

theorem Ring.inverse_eq_inv' {G₀ : Type u_3} [GroupWithZero G₀] : Eq inverse Inv.inv

def CommGroupWithZero.toCancelCommMonoidWithZero {G₀ : Type u_3} [CommGroupWithZero G₀] : CancelCommMonoidWithZero G₀

Equations

• Eq CommGroupWithZero.toCancelCommMonoidWithZero { toMonoid := MonoidWithZero.toMonoid, mul_comm := ⋯, toZero := MonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯, toIsLeftCancelMulZero := ⋯ }

def CommGroupWithZero.toDivisionCommMonoid {G₀ : Type u_3} [CommGroupWithZero G₀] : DivisionCommMonoid G₀

Equations

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

theorem div_mul_cancel_left₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (ha : Ne a 0) (b : G₀) : Eq (HDiv.hDiv a (HMul.hMul a b)) (Inv.inv b)

theorem mul_div_cancel_left_of_imp {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (h : Eq a 0 → Eq b 0) : Eq (HDiv.hDiv (HMul.hMul a b) a) b

theorem mul_div_cancel_of_imp' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (h : Eq b 0 → Eq a 0) : Eq (HMul.hMul b (HDiv.hDiv a b)) a

theorem mul_div_cancel₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {b : G₀} (a : G₀) (hb : Ne b 0) : Eq (HMul.hMul b (HDiv.hDiv a b)) a

theorem mul_div_mul_left {G₀ : Type u_3} [CommGroupWithZero G₀] {c : G₀} (a b : G₀) (hc : Ne c 0) : Eq (HDiv.hDiv (HMul.hMul c a) (HMul.hMul c b)) (HDiv.hDiv a b)

theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_3} [CommGroupWithZero G₀] {b d : G₀} (a c : G₀) (hb : Ne b 0) (hd : Ne d 0) (h : Eq (HDiv.hDiv a b) (HDiv.hDiv c d)) : Eq (HMul.hMul a d) (HMul.hMul c b)

theorem div_eq_div_iff {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hb : Ne b 0) (hd : Ne d 0) : Iff (Eq (HDiv.hDiv a b) (HDiv.hDiv c d)) (Eq (HMul.hMul a d) (HMul.hMul c b))

theorem div_eq_div_iff_div_eq_div' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hb : Ne b 0) (hc : Ne c 0) : Iff (Eq (HDiv.hDiv a b) (HDiv.hDiv c d)) (Eq (HDiv.hDiv a c) (HDiv.hDiv b d))

The CommGroupWithZero version of div_eq_div_iff_div_eq_div.

theorem div_div_cancel₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (ha : Ne a 0) : Eq (HDiv.hDiv a (HDiv.hDiv a b)) b

@[deprecated div_div_cancel₀ (since := "2024-11-25")]

theorem div_div_cancel' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (ha : Ne a 0) : Eq (HDiv.hDiv a (HDiv.hDiv a b)) b

Alias of div_div_cancel₀.

theorem div_div_cancel_left' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (ha : Ne a 0) : Eq (HDiv.hDiv (HDiv.hDiv a b) a) (Inv.inv b)

theorem div_helper {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (b : G₀) (h : Ne a 0) : Eq (HMul.hMul (HDiv.hDiv 1 (HMul.hMul a b)) a) (HDiv.hDiv 1 b)

theorem div_div_div_cancel_left' {G₀ : Type u_3} [CommGroupWithZero G₀] {c : G₀} (a b : G₀) (hc : Ne c 0) : Eq (HDiv.hDiv (HDiv.hDiv c a) (HDiv.hDiv c b)) (HDiv.hDiv b a)

theorem div_mul_div_cancel₀' {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (ha : Ne a 0) (b c : G₀) : Eq (HMul.hMul (HDiv.hDiv a b) (HDiv.hDiv c a)) (HDiv.hDiv c b)

noncomputable def groupWithZeroOfIsUnitOrEqZero {M : Type u_4} [Nontrivial M] [hM : MonoidWithZero M] (h : ∀ (a : M), Or (IsUnit a) (Eq 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.

noncomputable def commGroupWithZeroOfIsUnitOrEqZero {M : Type u_4} [Nontrivial M] [hM : CommMonoidWithZero M] (h : ∀ (a : M), Or (IsUnit a) (Eq a 0)) : CommGroupWithZero M

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

Equations

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