basic): golf rec_on_pos_prime_pos_coprime, remove import (#14935)

Commit

3 years ago

chore(data/nat/factorization/basic): golf rec_on_pos_prime_pos_coprime, remove import (#14935) Golf the proof of `rec_on_pos_prime_pos_coprime`, eliminating the need for `tactic.interval_cases`

Author

stuart-presnell

Parents

ee8d588d

mathlib3 478773b8 - chore(data/nat/factorization/basic): golf rec_on_pos_prime_pos_coprime, remove import (#14935)

mathlib3
478773b8 - chore(data/nat/factorization/basic): golf rec_on_pos_prime_pos_coprime, remove import (#14935)