Field.zpow_succ'
theorem Field.zpow_succ' :
∀ {K : Type u} [self : Field K] (n : ℕ) (a : K), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a
This theorem states that for any field `K` and any natural number `n` and element `a` from `K`, the power of `a` raised to `n + 1` is equal to the power of `a` raised to `n` times `a`. This is a property of exponentiation in a field, resembling the similar property in the standard arithmetic: `a^(n + 1) = a^n * a`.
More concisely: For any field `K` and natural number `n`, the element `a` in `K` raised to the power `n + 1` equals the power of `a` raised to `n` multiplied by `a`. In mathematical notation: `a^(n + 1) = a^n * a`.
|
Rat.cast_mk'
theorem Rat.cast_mk' :
∀ {K : Type u_3} [inst : DivisionRing K] (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : a.natAbs.Coprime b),
↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a / ↑b
The theorem `Rat.cast_mk'` states that for any division ring `K`, given an integer `a`, a natural number `b` which is not zero, and assuming that the absolute value of `a` and `b` are coprime (i.e., their greatest common divisor is 1), then the rational number created with `a` as the numerator and `b` as the denominator, when cast as a member of `K`, is equivalent to `a` cast as a member of `K` multiplied by the inverse of `b` cast as a member of `K`. This theorem essentially describes a property of constructing and casting rational numbers in a division ring.
More concisely: Given a division ring K, an integer a, a non-zero natural number b with gcd(a, b) = 1, the casting of the rational number (a / b) to K is equivalent to casting a to K multiplied by the multiplicative inverse of b in K.
|
Field.zpow_zero'
theorem Field.zpow_zero' : ∀ {K : Type u} [self : Field K] (a : K), Field.zpow 0 a = 1
This theorem states that for any field `K` and any element `a` in `K`, the zeroth power of `a` is `1`. More formally, if `a` is an element of a field `K`, then `a` to the power of 0 equals 1, denoted as `a ^ 0 = 1`. This is a basic property of exponentiation in fields.
More concisely: For any field `K` and its element `a`, `a` raised to the power of 0 equals 1 (i.e., `a^0 = 1`).
|
DivisionRing.div_eq_mul_inv
theorem DivisionRing.div_eq_mul_inv : ∀ {α : Type u_4} [self : DivisionRing α] (a b : α), a / b = a * b⁻¹
This theorem states that for any division ring `α`, the division operation `a / b` is equivalent to multiplying `a` by the multiplicative inverse of `b`, or `a * b⁻¹`. This is a standard property of division in mathematics and this theorem formalizes this property for any type `α` that forms a division ring.
More concisely: For any division ring `α`, the division operation `a / b` is equal to the multiplicative inverse of `b` times `a`, i.e., `a / b = a * b⁻¹`.
|
DivisionSemiring.mul_inv_cancel
theorem DivisionSemiring.mul_inv_cancel : ∀ {α : Type u_4} [self : DivisionSemiring α] (a : α), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for any nonzero element 'a' of a Division Semiring (a type of mathematical structure), the product of 'a' and the inverse of 'a' is equal to 1. Essentially, it formalizes the property of invertibility in Division Semirings, where every nonzero element has an inverse such that when multiplied together, they yield the multiplicative identity, 1.
More concisely: In a Division Semiring, the product of any nonzero element and its multiplicative inverse is the multiplicative identity.
|
DivisionRing.zpow_succ'
theorem DivisionRing.zpow_succ' :
∀ {α : Type u_4} [self : DivisionRing α] (n : ℕ) (a : α),
DivisionRing.zpow (Int.ofNat n.succ) a = DivisionRing.zpow (Int.ofNat n) a * a
This theorem states that, for any division ring `α`, any element `a` of `α`, and any natural number `n`, the value of `a` raised to the power (`n + 1`) is equivalent to the value of `a` raised to the power `n`, multiplied by `a`. This corresponds to the mathematical property $a^{(n + 1)} = a^n * a$. This theorem extends the power operation to the integers in a division ring.
More concisely: For any division ring `α`, element `a` in `α`, and natural number `n`, `a^(n + 1)` equals `a^n * a`.
|
DivisionRing.zpow_zero'
theorem DivisionRing.zpow_zero' : ∀ {α : Type u_4} [self : DivisionRing α] (a : α), DivisionRing.zpow 0 a = 1 := by
sorry
The theorem `DivisionRing.zpow_zero'` states that for any number `a` from a division ring `α`, the zeroth power of `a` is equal to 1. This conforms to the general mathematical principle that any non-zero number raised to the power of zero is 1.
More concisely: For any element `a` in a division ring, `a^0 = 1`.
|
DivisionSemiring.inv_zero
theorem DivisionSemiring.inv_zero : ∀ {α : Type u_4} [self : DivisionSemiring α], 0⁻¹ = 0
This theorem states that in any division semiring (a structure similar to a ring, but with additional properties such as a multiplicative identity and the existence of multiplicative inverses for non-zero elements) the multiplicative inverse of zero is zero. That is, in such structures, the operation of taking the reciprocal of zero (denoted by "0⁻¹") returns zero.
More concisely: In any division semiring, the multiplicative identity for zero is zero. (Equivalent to: The multiplicative inverse of zero is zero.)
|
Field.zpow_neg'
theorem Field.zpow_neg' :
∀ {K : Type u} [self : Field K] (n : ℕ) (a : K), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹ := by
sorry
This theorem states that for any field `K`, any element `a` of `K`, and any natural number `n`, raising `a` to the power of `-(n + 1)` (which is represented as `Int.negSucc n` in Lean) equals the inverse of `a` raised to the power of `(n + 1)`. In mathematical notation, this theorem is saying that `a^-(n + 1) = (a^(n + 1))^(-1)`.
More concisely: For any field `K` and its element `a`, raising `a` to the power of `-(n + 1)` equals the inverse of `a` raised to the power of `(n + 1)` for any natural number `n`. In Lean, this is represented as `a^(Int.negSucc n) = (a^(n + 1))^(-1)`.
|
Semifield.mul_inv_cancel
theorem Semifield.mul_inv_cancel : ∀ {α : Type u_4} [self : Semifield α] (a : α), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for every non-zero element 'a' of a semifield 'α', the product of 'a' and its inverse equals one. That is, every non-zero element of a semifield is invertible, and when multiplied by its inverse, the result is the multiplicative identity of the field. This is a fundamental property of fields and semifields in algebra.
More concisely: Every non-zero element in a semifield has a multiplicative inverse and their product is equal to the multiplicative identity.
|
Semifield.zpow_neg'
theorem Semifield.zpow_neg' :
∀ {α : Type u_4} [self : Semifield α] (n : ℕ) (a : α),
Semifield.zpow (Int.negSucc n) a = (Semifield.zpow (↑n.succ) a)⁻¹
This theorem states that for any semifield, given a natural number `n` and an element `a` from the semifield, the power of `a` to the negative of `n + 1` (which is computed by the function `Semifield.zpow`) is equal to the inverse of `a` to the power of `n + 1`. Formally, `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`. This applies to all types `α` that have a `Semifield` structure.
More concisely: For any semifield `α` and natural number `n`, the negative power `a ^ -(n + 1)` equals the inverse of `a` raised to the power `n + 1`, i.e., `(a ^ (n + 1))⁻¹`.
|
DivisionRing.zpow_neg'
theorem DivisionRing.zpow_neg' :
∀ {α : Type u_4} [self : DivisionRing α] (n : ℕ) (a : α),
DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
This theorem, `DivisionRing.zpow_neg'`, states that for any division ring `α`, any natural number `n`, and any element `a` of `α`, the negative superpower operation is equivalent to the inverse of the positive superpower operation. More precisely, raising `a` to the power of the negative of the successor of `n` (`a ^ -(n + 1)`) is the same as the inverse of raising `a` to the power of the successor of `n` (`(a ^ (n + 1))⁻¹`). The successor function in Lean represents the natural number operation of adding one.
More concisely: For any division ring `α` and natural number `n`, the negative superpower `a ^ -(n + 1)` equals the multiplicative inverse of `a ^ (n + 1)`, i.e., `(a ^ (n + 1))⁻¹`.
|
DivisionSemiring.div_eq_mul_inv
theorem DivisionSemiring.div_eq_mul_inv : ∀ {α : Type u_4} [self : DivisionSemiring α] (a b : α), a / b = a * b⁻¹ := by
sorry
The theorem `DivisionSemiring.div_eq_mul_inv` asserts that for any given type `α` which is a DivisionSemiring, division operation `a / b` is equivalent to multiplication of `a` with the multiplicative inverse of `b`, i.e., `a * b⁻¹`. Here `a` and `b` are elements of the type `α`.
More concisely: For any type `α` that is a DivisionSemiring, the division operation `a / b` equals the multiplication of `a` with the multiplicative inverse of `b`, i.e., `a * b⁻¹`.
|
DivisionSemiring.zpow_succ'
theorem DivisionSemiring.zpow_succ' :
∀ {α : Type u_4} [self : DivisionSemiring α] (n : ℕ) (a : α),
DivisionSemiring.zpow (Int.ofNat n.succ) a = DivisionSemiring.zpow (Int.ofNat n) a * a
This theorem asserts that for any division semiring `α`, and for any natural number `n` and element `a` of `α`, the `zpow` operation which represents integer exponents, obeys the property that `a` to the power of `(n + 1)` is equal to `a` to the power of `n` multiplied by `a`. In other words, it states the familiar rule from basic algebra that the `n+1`-th power of `a` can be computed by multiplying the `n`-th power of `a` by `a` itself.
More concisely: For any division semiring `α` and natural number `n`, the `zpow` operation satisfies `zpow a (n + 1) = zpow a n * a`.
|
DivisionRing.mul_inv_cancel
theorem DivisionRing.mul_inv_cancel : ∀ {α : Type u_4} [self : DivisionRing α] (a : α), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for any given division ring `α` and a non-zero element `a` of type `α`, the multiplicative inverse `a⁻¹` of `a` acts as a right multiplicative inverse. In other words, when `a` is multiplied by its inverse `a⁻¹`, the result is the multiplicative identity element `1` of the division ring. This is a fundamental property in the field of group theory and abstract algebra.
More concisely: For any division ring `α` and non-zero element `a` of type `α`, `a * a⁻¹ = 1`.
|
DivisionSemiring.zpow_zero'
theorem DivisionSemiring.zpow_zero' :
∀ {α : Type u_4} [self : DivisionSemiring α] (a : α), DivisionSemiring.zpow 0 a = 1
The theorem `DivisionSemiring.zpow_zero'` states that for any type `α` that forms a division semiring, for any element `a` of type `α`, raising `a` to the power of 0 results in 1. In other words, it asserts the common mathematical rule that anything to the power of 0 is equal to 1, in the context of a division semiring.
More concisely: For any division semiring `α`, the power `a^0` of any element `a` in `α` equals the multiplicative identity `1`.
|
Field.mul_inv_cancel
theorem Field.mul_inv_cancel : ∀ {K : Type u} [self : Field K] (a : K), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for any field `K` and any nonzero element `a` of `K`, multiplying `a` by its multiplicative inverse `a⁻¹` from the right gives the multiplicative identity, which is `1`. Therefore, `a⁻¹` is the right multiplicative inverse of `a`.
More concisely: For any field `K` and nonzero element `a` in `K`, `a * a⁻¹ = 1`. Thus, `a⁻¹` is the right identity with respect to multiplication for `a`.
|
Semifield.zpow_zero'
theorem Semifield.zpow_zero' : ∀ {α : Type u_4} [self : Semifield α] (a : α), Semifield.zpow 0 a = 1
The theorem `Semifield.zpow_zero'` states that for any type `α` that forms a semifield, raising any element `a` of this semifield to the power 0 results in 1. This mirrors the commonly known rule in mathematics, where any number raised to the power of 0 is 1.
More concisely: For any semifield `α`, `a^0 = 1` for all `a : α`.
|
Semifield.zpow_succ'
theorem Semifield.zpow_succ' :
∀ {α : Type u_4} [self : Semifield α] (n : ℕ) (a : α),
Semifield.zpow (Int.ofNat n.succ) a = Semifield.zpow (Int.ofNat n) a * a
This theorem states that for any natural number `n` and any element `a` from a Semifield structure, the power of `a` raised to the quantity of `n + 1` is equal to the power of `a` raised to `n` multiplied by `a`. In mathematical terms, this can be written as `a^(n + 1) = a^n * a`. This theorem is a fundamental property of exponentiation in the context of Semifields.
More concisely: For any natural number `n` and semigroup element `a`, `a^(n + 1) = a^n * a`.
|
Rat.smul_def
theorem Rat.smul_def : ∀ {K : Type u_3} [inst : DivisionRing K] (a : ℚ) (x : K), a • x = ↑a * x
This theorem, `Rat.smul_def`, states that for any division ring `K` and any rational number `a` and element `x` of `K`, the scalar multiplication of `a` and `x` (notated as `a • x`) is equal to the multiplication of the real number representation of `a` (notated as `↑a`) and `x`. This essentially says that scalar multiplication in the division ring works as you'd intuitively expect from real number multiplication.
More concisely: For any division ring K and rational number a, the operation a • x of scalar multiplication equals the multiplication of the real number ↑a and element x, i.e., a • x = ↑a * x.
|
Semifield.div_eq_mul_inv
theorem Semifield.div_eq_mul_inv : ∀ {α : Type u_4} [self : Semifield α] (a b : α), a / b = a * b⁻¹
This theorem, `Semifield.div_eq_mul_inv`, states that in any semifield `α`, the division operation could be defined as the multiplication of the first operand 'a' and the multiplicative inverse of the second operand 'b'. In other words, for any two elements 'a' and 'b' in the semifield `α`, the expression 'a / b' is equivalent to 'a * b⁻¹'. The `⁻¹` symbol represents the multiplicative inverse of 'b'.
More concisely: In a semifield, division equals multiplication with the multiplicative inverse.
|
Field.inv_zero
theorem Field.inv_zero : ∀ {K : Type u} [self : Field K], 0⁻¹ = 0
This theorem states that the inverse of zero (`0`) in a field (`K`) is conventionally defined as zero (`0`). This is a universal property, meaning it holds for all types `K` that have a field structure.
More concisely: In all fields, the additive and multiplicative identities are equal as inverses, that is, `0 = (0 : K).add_inv` and `1 = (1 : K).mul_inv`.
|
DivisionSemiring.zpow_neg'
theorem DivisionSemiring.zpow_neg' :
∀ {α : Type u_4} [self : DivisionSemiring α] (n : ℕ) (a : α),
DivisionSemiring.zpow (Int.negSucc n) a = (DivisionSemiring.zpow (↑n.succ) a)⁻¹
The theorem `DivisionSemiring.zpow_neg'` asserts that, for any division semiring `α`, any natural number `n`, and any element `a` from the semiring, the power operation of `a` raised to the negative of `n + 1` is equivalent to the inverse of `a` raised to `n + 1`. In other words, `a ^ -(n + 1) = (a ^ (n + 1))⁻¹` in the context of the division semiring.
More concisely: For any division semiring `α` and natural number `n`, `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`.
|
DivisionRing.inv_zero
theorem DivisionRing.inv_zero : ∀ {α : Type u_4} [self : DivisionRing α], 0⁻¹ = 0
This theorem states that in any division ring `α`, the multiplicative inverse of `0` is also `0`. In other words, if you take '0' and try to find its multiplicative reciprocal (notated as '0⁻¹'), you will get '0'. This is a convention used in mathematics and it is true in all division rings.
More concisely: In any division ring, the multiplicative identity is equal to the additive identity, that is, 0 has no multiplicative inverse.
|
Rat.cast_def
theorem Rat.cast_def : ∀ {K : Type u_3} [inst : DivisionRing K] (q : ℚ), ↑q = ↑q.num / ↑q.den
This theorem states that for any type `K` that is a division ring, the casting of a rational number `r` to type `K` is equivalent to the division of the casting of its numerator by the casting of its denominator. Essentially, it's showing how rational numbers are represented in any division ring.
More concisely: For any division ring K and rational number r = p / q, the casting of r to type K is equivalent to the division of the casting of p by the casting of q in K. (i.e., p / q in Q ≈ (p / q)_K)
|
Semifield.inv_zero
theorem Semifield.inv_zero : ∀ {α : Type u_4} [self : Semifield α], 0⁻¹ = 0
This theorem states that in any semifield, the multiplicative inverse (denoted by the superscript -1) of the element `0` is `0` itself. In other words, in the context of any semifield, when you take the multiplicative inverse of `0`, you will always get `0`.
More concisely: In any semifield, the multiplicative identity element is `0`. (This is equivalent to saying that the multiplicative inverse of `0` is `0`.)
|
Field.div_eq_mul_inv
theorem Field.div_eq_mul_inv : ∀ {K : Type u} [self : Field K] (a b : K), a / b = a * b⁻¹
The theorem `Field.div_eq_mul_inv` states that for any field `K` and for any elements `a` and `b` of that field, the division of `a` by `b` is equivalent to the multiplication of `a` by the multiplicative inverse of `b`. In mathematical terms, this is expressed as `a / b = a * b⁻¹.`
More concisely: For any field `K` and elements `a` and `b` of `K`, `a / b = a * b⁻¹`.
|