Int.units_eq_one_or
theorem Int.units_eq_one_or : ∀ (u : ℤˣ), u = 1 ∨ u = -1
This theorem states that for any unit `u` in the set of integers, `u` is either equal to 1 or -1. So, in the language of integers, the only unit (an element with a multiplicative inverse) elements are 1 and -1.
More concisely: In the realm of integers, only 1 and -1 are units (have multiplicative inverses).
|
Int.IsUnit.natAbs_eq
theorem Int.IsUnit.natAbs_eq : ∀ {n : ℤ}, IsUnit n → n.natAbs = 1
This theorem, named `Int.IsUnit.natAbs_eq`, states that for any integer `n`, if `n` is a unit in the monoid of integers (which means `n` has a two-sided inverse), then the absolute value of `n` (represented as a natural number) is equal to 1. This is essentially an alias for the forward direction of another theorem called `Int.isUnit_iff_natAbs_eq`.
More concisely: If an integer is a unit in the monoid of integers, then its absolute value equals 1.
|
Int.isUnit_eq_one_or
theorem Int.isUnit_eq_one_or : ∀ {a : ℤ}, IsUnit a → a = 1 ∨ a = -1
This theorem states that for every integer `a`, if `a` is a unit in the monoid of integers, then `a` is equal to 1 or `a` is equal to -1. In mathematical terms, a unit in a monoid is an element that has a multiplicative inverse. Hence, in the context of integers, this theorem basically says that the only units (elements that have a multiplicative inverse) are 1 and -1, as these are the only integers whose product with another integer results in the multiplicative identity, i.e., 1.
More concisely: In the monoid of integers, the only units are 1 and -1.
|
Int.isUnit_iff
theorem Int.isUnit_iff : ∀ {a : ℤ}, IsUnit a ↔ a = 1 ∨ a = -1
The theorem `Int.isUnit_iff` states that for any integer `a`, `a` is a unit if and only if `a` is either 1 or -1. In the context of monoids, a unit is an element that has a two-sided inverse. Here, the `IsUnit` predicate is used to identify such elements. For the set of integers under multiplication, the only units are 1 and -1, since these are the only integers that have two-sided inverses.
More concisely: An integer is a unit if and only if it is equal to 1 or -1.
|
Int.isUnit_iff_natAbs_eq
theorem Int.isUnit_iff_natAbs_eq : ∀ {n : ℤ}, IsUnit n ↔ n.natAbs = 1
This theorem states that for any integer `n`, `n` is a unit in the monoid of integers if and only if the absolute value of `n` is `1`. In more mathematical terms, an integer `n` has a two-sided inverse (making it a unit) if and only if the absolute value of `n` (represented by `Int.natAbs n` in Lean) equals `1`. The two-sided inverse here would be the multiplicative inverse, as the integers form a monoid under multiplication.
More concisely: An integer `n` is a unit in the monoid of integers if and only if |n| = 1, where |n| represents the absolute value of `n`.
|