abs_pow
theorem abs_pow : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : α) (n : ℕ), |a ^ n| = |a| ^ n
This theorem asserts that for any element `a` of a linear ordered ring and for any natural number `n`, the absolute value of `a` raised to the power `n` is equivalent to the absolute value of `a` raised to the power `n`. In mathematical notation, this can be written as |a^n| = |a|^n.
More concisely: For any element `a` in a linear ordered ring and natural number `n`, the absolute value of `a` raised to the power `n` equals the absolute value of `a` raised to the power `n`. In symbols: |a^n| = |a|^n.
|
abs_one
theorem abs_one : ∀ {α : Type u_1} [inst : LinearOrderedRing α], |1| = 1
This theorem states that the absolute value of 1 is 1 for any type `α` that forms a linear ordered ring. In other words, no matter what specific number system we are working in, as long as it's a linear ordered ring, the absolute value of the number 1 will always be 1.
More concisely: For all types `α` that are linear ordered rings, |1| = 1.
|
abs_mul_self
theorem abs_mul_self : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : α), |a * a| = a * a
This theorem states that for any element 'a' from a linearly ordered ring 'α', the absolute value of the product of 'a' and itself is equal to the product of 'a' and itself. This is essentially saying that the square of any number in a linearly ordered ring is always non-negative, hence taking the absolute value doesn't change its value.
More concisely: For any element 'a' in a linearly ordered ring, |a^2| = |a| \* |a|.
|
sq_abs
theorem sq_abs : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : α), |a| ^ 2 = a ^ 2
This theorem, `sq_abs`, states that for any given element `a` of a type `α`, where `α` is a linear ordered ring, the square of the absolute value of `a` is equal to the square of `a` itself. In mathematical terms, it says that for all `a` in `α`, |a|^2 = a^2. This is a property related to the definition of absolute values in a linear ordered ring.
More concisely: For any element `a` in a linear ordered ring `α`, |a|^2 = a^2.
|
sq_lt_sq
theorem sq_lt_sq : ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a b : α}, a ^ 2 < b ^ 2 ↔ |a| < |b|
The theorem `sq_lt_sq` states that for any type `α` that is a linear ordered ring, and for any two elements (`a` and `b`) of this type, `a` squared is less than `b` squared if and only if the absolute value of `a` is less than the absolute value of `b`. In mathematical terms, it is expressed as \(a^2 < b^2 \Leftrightarrow |a| < |b|\).
More concisely: For any linear ordered ring type `α` and its elements `a` and `b`, `a`'s square is less than `b`'s square if and only if the absolute value of `a` is less than the absolute value of `b`. In mathematical notation, `a² < b² ↔ |a| < |b|`.
|
sq_le_sq
theorem sq_le_sq : ∀ {α : Type u_1} [inst : LinearOrderedRing α] {a b : α}, a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
This theorem, `sq_le_sq`, states that for any type `α` that has a structure of a linearly ordered ring, the square of any element `a` of this type is less than or equal to the square of any other element `b` if and only if the absolute value of `a` is less than or equal to the absolute value of `b`. In mathematical terms, for any `a` and `b` in the linearly ordered ring `α`, `a^2 ≤ b^2` is equivalent to `|a| ≤ |b|`.
More concisely: In a linearly ordered ring, the square of an element is less than or equal to the square of another element if and only if the absolute values of the elements are in that order.
|
abs_mul_abs_self
theorem abs_mul_abs_self : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : α), |a| * |a| = a * a
This theorem states that for any type `α` which is a LinearOrderedRing, the absolute value of an element `a` from this ring multiplied by itself is equal to `a` multiplied by itself. In mathematical terms, for all `a` in a LinearOrderedRing `α`, we have `|a| * |a| = a * a`. This theorem generalizes the fact that the square of the absolute value of a real number is equal to the square of the number itself.
More concisely: For any linear ordered ring `α` and its element `a`, the absolute value of `a` squared equals `a` multiplied by itself: `|a| * |a| = a * a`.
|
abs_mul
theorem abs_mul : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a b : α), |a * b| = |a| * |b|
This theorem, `abs_mul`, states that for any given type `α`, which is an instance of a `LinearOrderedRing`, the absolute value of the product of any two elements `a` and `b` of type `α` is equal to the product of the absolute values of `a` and `b`. In mathematical terms, it expresses that |a * b| = |a| * |b| for all a, b in a linear ordered ring.
More concisely: For any linear ordered ring (α, +, *, |.|), |a * b| = |a| * |b| for all a, b in α.
|
pow_abs
theorem pow_abs : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : α) (n : ℕ), |a| ^ n = |a ^ n|
This theorem, named `pow_abs`, states that for any type `α` that forms a linear ordered ring, the absolute value of `a` raised to the power of `n` is equal to the absolute value of `a` itself raised to the power of `n`. Here `a` is an element of the type `α` and `n` is a natural number. This effectively means that when exponentiation interacts with absolute value, the order of operations doesn't matter.
More concisely: For any linear ordered ring type `α` and natural number `n`, the absolute value of `a^n` equals the absolute value of `a` raised to the power `n` for all `a` in `α`.
|