Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

Modification history

2022-10-10 08:47

src/data/int/gcd.lean

chore(data/int/gcd): streamline imports (#16811) …

Modified int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul View on Github →

2018-08-31 17:48

data/int/basic.lean

refactor(data/int/gcd): move int gcd proofs to the GCD theory

Modified int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul View on Github →

2018-08-30 15:34

data/int/basic.lean

refactor(data/nat,int): separate int from nat, i.e. do not import any int theory in nat

Added int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul View on Github →