Cast of integers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
int_cast : ℤ → R
field.
Preferentially, the homomorphism is written as a coercion.
Main declarations #
int.cast
: Canonical homomorphismℤ → R
.add_group_with_one
: Type class forint.cast
.
@[class]
Type class for the canonical homomorphism ℤ → R
.
Instances of this typeclass
- subring_class.to_has_int_cast
- add_group_with_one.to_has_int_cast
- mul_opposite.has_int_cast
- add_opposite.has_int_cast
- pi.has_int_cast
- order_dual.has_int_cast
- lex.has_int_cast
- rat.has_int_cast
- ulift.has_int_cast
- ring_con.quotient.has_int_cast
- self_adjoint.has_int_cast
- polynomial.has_int_cast
- cau_seq.completion.Cauchy.has_int_cast
- real.has_int_cast
- direct_sum.has_int_cast
Instances of other typeclasses for has_int_cast
- has_int_cast.has_sizeof_inst
@[class]
- int_cast : ℤ → R
- add : R → R → R
- add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
- zero : R
- zero_add : ∀ (a : R), 0 + a = a
- add_zero : ∀ (a : R), a + 0 = a
- nsmul : ℕ → R → R
- nsmul_zero' : (∀ (x : R), add_group_with_one.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : R), add_group_with_one.nsmul n.succ x = x + add_group_with_one.nsmul n x) . "try_refl_tac"
- neg : R → R
- sub : R → R → R
- sub_eq_add_neg : (∀ (a b : R), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → R → R
- zsmul_zero' : (∀ (a : R), add_group_with_one.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : R), add_group_with_one.zsmul (int.of_nat n.succ) a = a + add_group_with_one.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : R), add_group_with_one.zsmul -[1+ n] a = -add_group_with_one.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : R), -a + a = 0
- nat_cast : ℕ → R
- one : R
- nat_cast_zero : add_group_with_one.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), add_group_with_one.nat_cast (n + 1) = add_group_with_one.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), add_group_with_one.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), add_group_with_one.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
An add_group_with_one
is an add_group
with a 1
.
It also contains data for the unique homomorphisms ℕ → R
and ℤ → R
.
Instances of this typeclass
- add_comm_group_with_one.to_add_group_with_one
- mul_opposite.add_group_with_one
- pi.add_group_with_one
- order_dual.add_group_with_one
- lex.add_group_with_one
- ulift.add_group_with_one
- prod.add_group_with_one
- cau_seq.add_group_with_one
- complex.add_group_with_one
- triv_sq_zero_ext.add_group_with_one
- quaternion_algebra.add_group_with_one
Instances of other typeclasses for add_group_with_one
- add_group_with_one.has_sizeof_inst
@[instance]
@[instance]
@[instance]
@[class]
- add : R → R → R
- add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
- zero : R
- zero_add : ∀ (a : R), 0 + a = a
- add_zero : ∀ (a : R), a + 0 = a
- nsmul : ℕ → R → R
- nsmul_zero' : (∀ (x : R), add_comm_group_with_one.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : R), add_comm_group_with_one.nsmul n.succ x = x + add_comm_group_with_one.nsmul n x) . "try_refl_tac"
- neg : R → R
- sub : R → R → R
- sub_eq_add_neg : (∀ (a b : R), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → R → R
- zsmul_zero' : (∀ (a : R), add_comm_group_with_one.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : R), add_comm_group_with_one.zsmul (int.of_nat n.succ) a = a + add_comm_group_with_one.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : R), add_comm_group_with_one.zsmul -[1+ n] a = -add_comm_group_with_one.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : R), -a + a = 0
- add_comm : ∀ (a b : R), a + b = b + a
- int_cast : ℤ → R
- nat_cast : ℕ → R
- one : R
- nat_cast_zero : add_comm_group_with_one.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), add_comm_group_with_one.nat_cast (n + 1) = add_comm_group_with_one.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), add_comm_group_with_one.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), add_comm_group_with_one.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
An add_comm_group_with_one
is an add_group_with_one
satisfying a + b = b + a
.
Instances of this typeclass
Instances of other typeclasses for add_comm_group_with_one
- add_comm_group_with_one.has_sizeof_inst
@[instance]
def
add_comm_group_with_one.to_add_comm_monoid_with_one
(R : Type u)
[self : add_comm_group_with_one R] :
@[instance]
@[instance]
@[protected]
Canonical homomorphism from the integers to any ring(-like) structure R
Equations
@[protected, instance]
Equations
- int.cast_coe = {coe := int.cast _inst_2}