Compfiles/Singapore2019P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 4

http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf

If $\log_{21} 3 = x$, express $\log_7 9$ in terms of $x$.

Imports (2)
Imported by 1 file
  1. determine Singapore2019R1P4.solution line 26 source

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

    Statement uses: Real

    Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, HSub.hSub

    12 instances, coercions and auxiliary constants left out.

  2. problem Singapore2019R1P4.singapore2019_r1_p4 line 28 source

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

    Statement uses: Real, Eq, Real.logb, OfNat.ofNat, Nat, Singapore2019R1P4.solution

    Proof uses: HDiv.hDiv, id, of_eq_true, Real.log, Eq.trans, inferInstance, CommGroupWithZero, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, HMul.hMul, congr_arg₂, rfl and 86 more

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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