Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.Units

Lemmas for units in an ordered monoid #

theorem Units.mulLECancellable_val {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

MulLECancellable ↑u

theorem Units.inv_mul_le_iff {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} :

↑u⁻¹ * a ≤ b ↔ a ≤ ↑u * b

theorem Units.le_inv_mul_iff {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} :

a ≤ ↑u⁻¹ * b ↔ ↑u * a ≤ b

@[simp]

theorem Units.one_le_inv {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

1 ≤ ↑u⁻¹ ↔ ↑u ≤ 1

@[simp]

theorem Units.inv_le_one {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

↑u⁻¹ ≤ 1 ↔ 1 ≤ ↑u

theorem Units.one_le_inv_mul {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a : M} :

1 ≤ ↑u⁻¹ * a ↔ ↑u ≤ a

theorem Units.inv_mul_le_one {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a : M} :

↑u⁻¹ * a ≤ 1 ↔ a ≤ ↑u

theorem Units.le_mul_of_inv_mul_le {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} :

↑u⁻¹ * a ≤ b → a ≤ ↑u * b

Alias of the forward direction of Units.inv_mul_le_iff.

theorem Units.inv_mul_le_of_le_mul {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} :

a ≤ ↑u * b → ↑u⁻¹ * a ≤ b

Alias of the reverse direction of Units.inv_mul_le_iff.

theorem Units.mul_le_of_le_inv_mul {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} :

a ≤ ↑u⁻¹ * b → ↑u * a ≤ b

Alias of the forward direction of Units.le_inv_mul_iff.

theorem Units.le_inv_mul_of_mul_le {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} :

↑u * a ≤ b → a ≤ ↑u⁻¹ * b

Alias of the reverse direction of Units.le_inv_mul_iff.

theorem Units.one_le_inv_of_le {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

↑u ≤ 1 → 1 ≤ ↑u⁻¹

Alias of the reverse direction of Units.one_le_inv.

theorem Units.le_of_one_le_inv {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

1 ≤ ↑u⁻¹ → ↑u ≤ 1

Alias of the forward direction of Units.one_le_inv.

theorem Units.inv_le_one_of_le {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

1 ≤ ↑u → ↑u⁻¹ ≤ 1

Alias of the reverse direction of Units.inv_le_one.

theorem Units.le_of_inv_le_one {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) :

↑u⁻¹ ≤ 1 → 1 ≤ ↑u

Alias of the forward direction of Units.inv_le_one.

theorem Units.le_of_one_le_inv_mul {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a : M} :

1 ≤ ↑u⁻¹ * a → ↑u ≤ a

Alias of the forward direction of Units.one_le_inv_mul.

theorem Units.one_le_inv_mul_of_le {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a : M} :

↑u ≤ a → 1 ≤ ↑u⁻¹ * a

Alias of the reverse direction of Units.one_le_inv_mul.

theorem Units.le_of_inv_mul_le_one {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a : M} :

↑u⁻¹ * a ≤ 1 → a ≤ ↑u

Alias of the forward direction of Units.inv_mul_le_one.

theorem Units.inv_mul_le_one_of_le {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a : M} :

a ≤ ↑u → ↑u⁻¹ * a ≤ 1

Alias of the reverse direction of Units.inv_mul_le_one.

theorem Units.mul_inv_le_iff {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b : M} (u : Mˣ) :

a * ↑u⁻¹ ≤ b ↔ a ≤ b * ↑u

theorem Units.le_mul_inv_iff {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b : M} (u : Mˣ) :

a ≤ b * ↑u⁻¹ ↔ a * ↑u ≤ b

theorem Units.one_le_mul_inv {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a : M} (u : Mˣ) :

1 ≤ a * ↑u⁻¹ ↔ ↑u ≤ a

theorem Units.mul_inv_le_one {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a : M} (u : Mˣ) :

a * ↑u⁻¹ ≤ 1 ↔ a ≤ ↑u

theorem Units.mul_inv_le_of_le_mul {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b : M} (u : Mˣ) :

a ≤ b * ↑u → a * ↑u⁻¹ ≤ b

Alias of the reverse direction of Units.mul_inv_le_iff.

theorem Units.le_mul_of_mul_inv_le {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b : M} (u : Mˣ) :

a * ↑u⁻¹ ≤ b → a ≤ b * ↑u

Alias of the forward direction of Units.mul_inv_le_iff.

theorem Units.mul_le_of_le_mul_inv {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b : M} (u : Mˣ) :

a ≤ b * ↑u⁻¹ → a * ↑u ≤ b

Alias of the forward direction of Units.le_mul_inv_iff.

theorem Units.le_mul_inv_of_mul_le {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b : M} (u : Mˣ) :

a * ↑u ≤ b → a ≤ b * ↑u⁻¹

Alias of the reverse direction of Units.le_mul_inv_iff.

theorem Units.le_of_one_le_mul_inv {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a : M} (u : Mˣ) :

1 ≤ a * ↑u⁻¹ → ↑u ≤ a

Alias of the forward direction of Units.one_le_mul_inv.

theorem Units.one_le_mul_inv_of_le {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a : M} (u : Mˣ) :

↑u ≤ a → 1 ≤ a * ↑u⁻¹

Alias of the reverse direction of Units.one_le_mul_inv.

theorem Units.le_of_mul_inv_le_one {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a : M} (u : Mˣ) :

a * ↑u⁻¹ ≤ 1 → a ≤ ↑u

Alias of the forward direction of Units.mul_inv_le_one.

theorem Units.mul_inv_le_one_of_le {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a : M} (u : Mˣ) :

a ≤ ↑u → a * ↑u⁻¹ ≤ 1

Alias of the reverse direction of Units.mul_inv_le_one.

theorem IsUnit.mulLECancellable {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] {a : M} (ha : IsUnit a) :

MulLECancellable a

theorem IsUnit.mul_le_mul_left {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] {a b c : M} (ha : IsUnit a) :

a * b ≤ a * c ↔ b ≤ c

theorem IsUnit.le_of_mul_le_mul_left {M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] {a b c : M} (ha : IsUnit a) :

a * b ≤ a * c → b ≤ c

Alias of the forward direction of IsUnit.mul_le_mul_left.

theorem IsUnit.mul_le_mul_right {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b c : M} (hc : IsUnit c) :

a * c ≤ b * c ↔ a ≤ b

theorem IsUnit.le_of_mul_le_mul_right {M : Type u_1} [Monoid M] [LE M] [MulRightMono M] {a b c : M} (hc : IsUnit c) :

a * c ≤ b * c → a ≤ b

Alias of the forward direction of IsUnit.mul_le_mul_right.