Mathlib.Data.Int.Cast.Defs

Module docstring

{"# Cast of integers

This file defines the canonical homomorphism from the integers into an additive group with a one (typically a Ring). In additive groups with a one element, there exists a unique such homomorphism and we store it in the intCast : ℤ → R field.

Preferentially, the homomorphism is written as a coercion.

Main declarations

Int.cast: Canonical homomorphism ℤ → R.
AddGroupWithOne: Type class for Int.cast. ","### Additive groups with one "}

Int.castDef definition

{R : Type u} [NatCast R] [Neg R] : ℤ → R

Full source

/-- Default value for `IntCast.intCast` in an `AddGroupWithOne`. -/
protected def Int.castDef {R : Type u} [NatCast R] [Neg R] : ℤ → R
  | (n : ℕ) => n
  | Int.negSucc n => -(n + 1 : ℕ)

Canonical integer cast function

Informal description

The function maps an integer \( n \) to its canonical image in a type \( R \) equipped with a natural number cast and negation. Specifically, for a non-negative integer \( n \), it returns \( n \) cast as an element of \( R \), and for a negative integer \( -\text{succ}(n) \), it returns the negation of \( (n + 1) \) cast as an element of \( R \).

AddGroupWithOne structure

(R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R

Full source

/-- An `AddGroupWithOne` is an `AddGroup` with a 1. It also contains data for the unique
homomorphisms `ℕ → R` and `ℤ → R`. -/
class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where
  /-- The canonical homomorphism `ℤ → R`. -/
  intCast := Int.castDef
  /-- The canonical homomorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`. -/
  intCast_ofNat : ∀ n : ℕ, intCast (n : ℕ) = Nat.cast n := by intros; rfl
  /-- The canonical homomorphism `ℤ → R` for negative values is just the negation of the values
  of the canonical homomorphism `ℕ → R`. -/
  intCast_negSucc : ∀ n : ℕ, intCast (Int.negSucc n) = - Nat.cast (n + 1) := by intros; rfl

Additive group with one

Informal description

An `AddGroupWithOne` is an additive group equipped with a distinguished element `1` and canonical homomorphisms from the natural numbers and integers. Specifically, it extends the structure of an `AddGroup` with the properties of `IntCast` (for integer coercion) and `AddMonoidWithOne` (for natural number coercion and the additive monoid structure with a one).

AddCommGroupWithOne structure

(R : Type u)
  extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R

Full source

/-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/
class AddCommGroupWithOne (R : Type u)
  extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R

Additive Commutative Group with One

Informal description

An `AddCommGroupWithOne` is an additive commutative group with a distinguished element `1` that satisfies the following properties: 1. It is an additive commutative group (i.e., the addition operation is commutative). 2. It has a canonical map from the integers (via `IntCast`). 3. It extends the structure of an additive group with one (`AddGroupWithOne`). 4. It extends the structure of an additive commutative monoid with one (`AddCommMonoidWithOne`). This structure combines the properties of being an additive commutative group with the additional structure provided by having a multiplicative identity element and integer casting.