Int.cast_pow
theorem Int.cast_pow : ∀ {R : Type u_1} [inst : Ring R] (n : ℤ) (m : ℕ), ↑(n ^ m) = ↑n ^ m
This theorem, named `Int.cast_pow`, states that for any integer (`ℤ`) `n` and natural number (`ℕ`) `m`, the result of casting (`↑`) the power of `n` and `m` (expressed as `n ^ m`) to a generic Ring type `R`, is equal to the result of casting `n` to `R` and then calculating the power with `m` (expressed as `↑n ^ m`). In other words, the order of the power operation and the cast operation can be interchanged without affecting the end result.
More concisely: For any integer `n`, natural number `m`, and ring `R`, the cast `↑(n ^ m)` is equal to `↑(n ^ m)` in `R`. In other words, the application of ring exponentiation and casting can be interchanged.
|
Int.cast_mul
theorem Int.cast_mul : ∀ {α : Type u_1} [inst : NonAssocRing α] (m n : ℤ), ↑(m * n) = ↑m * ↑n
This theorem states that for any non-associative ring `α` and any two integers `m` and `n`, the integer cast of their product (`m * n`) is equal to the product of their integer casts. In other words, multiplication commutes with the operation of integer casting in the context of a non-associative ring.
More concisely: For any non-associative ring `α` and integers `m` and `n`, the conversion of `m * n` to `α` is equal to the conversion of `m` to `α` multiplied by the conversion of `n` to `α`. In Lean notation: `(cast α m) * (cast α n) = cast α (m * n)`.
|