## Stream: new members

### Topic: Tactic for Divisibility

#### Andre Hernandez-Espiet (Rutgers) (Nov 04 2022 at 19:44):

I was wondering if there is a tactic that takes care of simple modular conditions. For example, a tactic that would solve the following, which is trivial on paper:

example {q a b x abar: ℤ } (div: q∣a*x+b) (abar_is: q∣ abar*a-1) : q∣ x+abar*b :=
begin
cases div with z hz,
cases abar_is with zz hzz,
have := congr_arg (has_mul.mul abar) hz,
rw [mul_add , ← mul_assoc] at this,
use (abar*z-zz*x),
rw [mul_sub,← mul_assoc q zz,← hzz, mul_comm abar z, ← mul_assoc, ← hz],
ring,
end


#### Ruben Van de Velde (Nov 04 2022 at 19:53):

example {q a b x abar: ℤ} (div : q ∣ a * x + b) (abar_is : q ∣ abar * a - 1) : q ∣ x + abar * b :=
begin
convert div.linear_comb abar_is abar (-x) using 1,
ring,
end


#### Andre Hernandez-Espiet (Rutgers) (Nov 04 2022 at 20:12):

Yes, that works! Very creative. I didn't even know convert could work with divides statements.

#### Kevin Buzzard (Nov 04 2022 at 20:23):

convert works with anything! tactic#convert let's see if there's a useful description in the docs. Edit: there is!

Last updated: Dec 20 2023 at 11:08 UTC