Compfiles/Usa1972P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1972, Problem 1

Let (a, b, ... , k) denote the greatest common divisor of the integers a, b, ... k and [a, b, ... , k] denote their least common multiple.

Show that for any positive integers a, b, c we have (a, b, c)² [a, b] [b, c] [c, a] = [a, b, c]² (a, b) (b, c) (c, a).

Imports (2)
Imported by 1 file
  1. problem Usa1972P1.usa1972_p1 line 44 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Eq, HMul.hMul, HPow.hPow, Nat.gcd, OfNat.ofNat, Nat.lcm

    Proof uses: dite, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Nat.gcd_zero_left, Nat.lcm_zero_left, MulZeroClass.mul_zero, MulZeroClass.zero_mul, Nat.lcm_zero_right, zero_pow, Not, False, not_false_eq_true, Nat.gcd_zero_right, eq_self, Nat.eq_of_factorization_eq, Eq.mpr and 20 more

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

    Open to load the checked before-and-after goal states.