Divisibility over ℕ and ℤ #
This file collects results for the integers and natural numbers that use abstract algebra in their proofs or cases of ℕ and ℤ being examples of structures in abstract algebra.
Main statements #
nat.factors_eq
: the multiset of elements ofnat.factors
is equal to the factors given by theunique_factorization_monoid
instance- ℤ is a
normalization_monoid
- ℤ is a
gcd_monoid
Tags #
prime, irreducible, natural numbers, integers, normalization monoid, gcd monoid, greatest common divisor, prime factorization, prime factors, unique factorization, unique factors
@[protected, instance]
ℕ
is a gcd_monoid.
Equations
- nat.gcd_monoid = {gcd := nat.gcd, lcm := nat.lcm, gcd_dvd_left := nat.gcd_dvd_left, gcd_dvd_right := nat.gcd_dvd_right, dvd_gcd := nat.gcd_monoid._proof_1, gcd_mul_lcm := nat.gcd_monoid._proof_2, lcm_zero_left := nat.lcm_zero_left, lcm_zero_right := nat.lcm_zero_right}
@[protected, instance]
Equations
- nat.normalized_gcd_monoid = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit infer_instance, norm_unit_zero := nat.normalized_gcd_monoid._proof_1, norm_unit_mul := nat.normalized_gcd_monoid._proof_2, norm_unit_coe_units := nat.normalized_gcd_monoid._proof_3}, to_gcd_monoid := {gcd := gcd_monoid.gcd infer_instance, lcm := gcd_monoid.lcm infer_instance, gcd_dvd_left := nat.normalized_gcd_monoid._proof_4, gcd_dvd_right := nat.normalized_gcd_monoid._proof_5, dvd_gcd := nat.normalized_gcd_monoid._proof_6, gcd_mul_lcm := nat.normalized_gcd_monoid._proof_7, lcm_zero_left := nat.normalized_gcd_monoid._proof_8, lcm_zero_right := nat.normalized_gcd_monoid._proof_9}, normalize_gcd := nat.normalized_gcd_monoid._proof_10, normalize_lcm := nat.normalized_gcd_monoid._proof_11}
@[protected, instance]
Equations
- int.normalization_monoid = {norm_unit := λ (a : ℤ), ite (0 ≤ a) 1 (-1), norm_unit_zero := int.normalization_monoid._proof_3, norm_unit_mul := int.normalization_monoid._proof_4, norm_unit_coe_units := int.normalization_monoid._proof_5}
theorem
int.eq_of_associated_of_nonneg
{a b : ℤ}
(h : associated a b)
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
a = b
@[protected, instance]
Equations
- int.gcd_monoid = {gcd := λ (a b : ℤ), ↑(a.gcd b), lcm := λ (a b : ℤ), ↑(a.lcm b), gcd_dvd_left := int.gcd_monoid._proof_3, gcd_dvd_right := int.gcd_monoid._proof_4, dvd_gcd := int.gcd_monoid._proof_5, gcd_mul_lcm := int.gcd_monoid._proof_6, lcm_zero_left := int.gcd_monoid._proof_7, lcm_zero_right := int.gcd_monoid._proof_8}
@[protected, instance]
Equations
- int.normalized_gcd_monoid = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit int.normalization_monoid, norm_unit_zero := int.normalized_gcd_monoid._proof_3, norm_unit_mul := int.normalized_gcd_monoid._proof_4, norm_unit_coe_units := int.normalized_gcd_monoid._proof_5}, to_gcd_monoid := {gcd := gcd_monoid.gcd infer_instance, lcm := gcd_monoid.lcm infer_instance, gcd_dvd_left := int.normalized_gcd_monoid._proof_6, gcd_dvd_right := int.normalized_gcd_monoid._proof_7, dvd_gcd := int.normalized_gcd_monoid._proof_8, gcd_mul_lcm := int.normalized_gcd_monoid._proof_9, lcm_zero_left := int.normalized_gcd_monoid._proof_10, lcm_zero_right := int.normalized_gcd_monoid._proof_11}, normalize_gcd := int.normalized_gcd_monoid._proof_12, normalize_lcm := int.normalized_gcd_monoid._proof_13}
Maps an associate class of integers consisting of -n, n
to n : ℕ
Equations
- associates_int_equiv_nat = {to_fun := λ (z : associates ℤ), z.out.nat_abs, inv_fun := λ (n : ℕ), associates.mk ↑n, left_inv := associates_int_equiv_nat._proof_2, right_inv := associates_int_equiv_nat._proof_3}
theorem
nat.factors_multiset_prod_of_irreducible
{s : multiset ℕ}
(h : ∀ (x : ℕ), x ∈ s → irreducible x) :
@[protected, instance]
Equations
- multiplicity.decidable_nat = λ (a b : ℕ), decidable_of_iff (a ≠ 1 ∧ 0 < b) _
@[protected, instance]
Equations
- multiplicity.decidable_int = λ (a b : ℤ), decidable_of_iff (a.nat_abs ≠ 1 ∧ b ≠ 0) _