Commit 2023-03-21 13:00 cff1de2e

View on Github →

feat: port RingTheory.Int.Basic (#3014)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Int/Basic.lean

added theorem Int.Prime.dvd_mul'

added theorem Int.Prime.dvd_mul

added theorem Int.Prime.dvd_pow'

added theorem Int.Prime.dvd_pow

added theorem Int.abs_eq_normalize

added theorem Int.associated_iff

added theorem Int.associated_iff_natAbs

added theorem Int.associated_natAbs

added theorem Int.coe_gcd

added theorem Int.coe_lcm

added theorem Int.coprime_iff_nat_coprime

added theorem Int.eq_of_associated_of_nonneg

added theorem Int.eq_pow_of_mul_eq_pow_bit1

added theorem Int.eq_pow_of_mul_eq_pow_bit1_left

added theorem Int.eq_pow_of_mul_eq_pow_bit1_right

added theorem Int.exists_prime_and_dvd

added theorem Int.exists_unit_of_abs

added theorem Int.gcd_eq_natAbs

added theorem Int.gcd_eq_one_iff_coprime

added theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_left

added theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_right

added theorem Int.gcd_ne_one_iff_gcd_mul_right_ne_one

added theorem Int.natAbs_euclideanDomain_gcd

added theorem Int.natAbs_gcd

added theorem Int.natAbs_lcm

added theorem Int.nonneg_iff_normalize_eq_self

added theorem Int.nonneg_of_normalize_eq_self

added theorem Int.normUnit_eq

added theorem Int.normalize_coe_nat

added theorem Int.normalize_of_nonneg

added theorem Int.normalize_of_nonpos

added theorem Int.prime_iff_natAbs_prime

added theorem Int.span_natAbs

added theorem Int.sq_of_coprime

added theorem Int.sq_of_gcd_eq_one

added theorem Int.zmultiples_natAbs

added theorem Nat.factors_eq

added theorem Nat.factors_multiset_prod_of_irreducible

added def associatesIntEquivNat

added theorem gcd_eq_nat_gcd

added theorem induction_on_primes

added theorem lcm_eq_nat_lcm

added theorem multiplicity.finite_int_iff

added theorem multiplicity.finite_int_iff_natAbs_finite

added theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two