Mathlib.Data.Int.CharZero._auxLemma.1
theorem Mathlib.Data.Int.CharZero._auxLemma.1 :
∀ {α : Type u_1} [inst : AddGroupWithOne α] [inst_1 : CharZero α] {n : ℤ}, (↑n = 0) = (n = 0)
This theorem states that for any type `α` which is an instance of `AddGroupWithOne` and `CharZero`, and for any integer `n`, the coercion of `n` to `α` equals zero if and only if `n` itself equals zero. In simpler terms, this theorem says that an integer `n` is equal to zero only if its representation in the type `α` is also zero. This is under the condition that the type `α` allows for addition, has a multiplicative identity, and has a characteristic of zero (which means that there is no positive integer `n` for which `n` times the multiplicative identity equals zero).
More concisely: For any type `α` that is an instance of `AddGroupWithOne` and `CharZero`, the coercion of an integer `n` to `α` equals the multiplicative identity if and only if `n` equals zero.
|
Mathlib.Data.Int.CharZero._auxLemma.2
theorem Mathlib.Data.Int.CharZero._auxLemma.2 :
∀ {α : Type u_1} [inst : AddGroupWithOne α] [inst_1 : CharZero α] {m n : ℤ}, (↑m = ↑n) = (m = n)
The theorem states that for any type 'α', if 'α' forms an additive group with unity (a mathematical structure with addition operation, a neutral element "one", and inverse elements), and if 'α' has characteristic zero (in other words, no natural number is equivalent to zero unless it is zero itself), then for any two integers 'm' and 'n', the equality of 'm' and 'n' as elements of 'α' (expressed by ↑m = ↑n) is equivalent to the equality of 'm' and 'n' as integers. Essentially, this theorem bridges the equality in integers and the equality in the abstract type 'α'.
More concisely: In an additive group with unity and characteristic zero 'α', the equality of integers 'm' and 'n' is equivalent to the equality of their corresponding elements in 'α' (i.e., ↑m = ↑n).
|
Int.cast_ne_zero
theorem Int.cast_ne_zero : ∀ {α : Type u_1} [inst : AddGroupWithOne α] [inst_1 : CharZero α] {n : ℤ}, ↑n ≠ 0 ↔ n ≠ 0
The theorem `Int.cast_ne_zero` states that for any type `α` that forms an additive group with a distinguished element of one (`AddGroupWithOne α`) and has no non-zero integers that map to the same element (`CharZero α`), an integer `n` is non-zero if and only if its cast to `α` is non-zero. In other words, casting a non-zero integer to this type will never result in zero.
More concisely: For any additive group with a multiplicative identity `α` satisfying `AddGroupWithOne α` and `CharZero α`, the integer `n` is non-zero if and only if its cast to `α` is non-zero.
|
Int.cast_injective
theorem Int.cast_injective :
∀ {α : Type u_1} [inst : AddGroupWithOne α] [inst_1 : CharZero α], Function.Injective Int.cast
The theorem `Int.cast_injective` states that for any type `α` that is an additive group with one (meaning it has a structure of an additive group with a distinct element identified as one), and that has the property of `CharZero` (meaning that any distinct integers map to distinct elements in `α`), the canonical function that casts an integer to an element of `α` is injective. In other words, distinct integers will always map to distinct elements of `α` under this casting function. This injection property guarantees that no information is lost when integers are cast to `α`, as the original integer can be uniquely recovered.
More concisely: The canonical function from integers to an additive group with one and CharZero structure maps distinct integers to distinct group elements.
|
Int.cast_inj
theorem Int.cast_inj : ∀ {α : Type u_1} [inst : AddGroupWithOne α] [inst_1 : CharZero α] {m n : ℤ}, ↑m = ↑n ↔ m = n
This theorem, `Int.cast_inj`, states that for any type `α` that has an `AddGroupWithOne` and `CharZero` structure, the equality of the casted integers `m` and `n` to type `α` implies and is implied by the equality of `m` and `n` themselves. In simpler terms, casting does not change the equality relationship between two integers, `m` and `n`, in the context of an additive group with one and a characteristic zero type.
More concisely: For any type `α` with an AddGroupWithOne and CharZero structure, the casted integers `m` and `n` are equal if and only if `m` and `n` are equal as integers.
|