Int.units_pow_two
theorem Int.units_pow_two : ∀ (u : ℤˣ), u ^ 2 = 1
This theorem, `Int.units_pow_two`, states that for any unit integer `u` (denoted as `ℤˣ`), the square of `u`, i.e., `u ^ 2`, is always equal to 1. In other words, when any unit integer is squared, the result is always 1.
More concisely: For any unit integer `u`, `u` raised to the power of 2 equals 1.
|
Int.units_mul_self
theorem Int.units_mul_self : ∀ (u : ℤˣ), u * u = 1
This theorem states that for every unit `u` in the set of units of integers `ℤˣ`, multiplying `u` by itself always yields 1. In other words, this theorem defines that every unit in the integer ring is its own multiplicative inverse.
More concisely: Every unit in the integers has multiplicative inverse and equals it in the multiplication, i.e., for all units `u` in `ℤˣ`, `u * u = 1`.
|
Int.units_sq
theorem Int.units_sq : ∀ (u : ℤˣ), u ^ 2 = 1
This theorem states that for any unit `u` of integers (`ℤˣ`), the square of `u` is equal to `1`. In the language of mathematics, this can be expressed as: for all `u` in the unit group of integers, `u^2 = 1`.
More concisely: For all units `u` in the integers, `u^2 = 1`.
|