number of odd

Stream: new members

[vxctyxeha]

hello i try to prove I am trying to prove a mathematical problem of a biased algorithm.Let ( n ) be a four-digit number with no leading zeroes and no repeated digits. Prove that if ( n ) is odd, the number of such ( n ) is 2240. Is there a way to avoid complex discussions?

import Mathlib

open Finset

theorem four_digit_odd_no_repeat :
    {n : ℕ | n ∈ Icc 1000 9999 ∧ Odd n ∧ (n.digits 10).Nodup}.ncard = 2240 := by
  have h1 : {n : ℕ | n ∈ Icc 1000 9999 ∧ Odd n ∧ (n.digits 10).Nodup} = Finset.filter (fun n => Odd n ∧ (n.digits 10).Nodup) (Icc 1000 9999) := by
    ext n
    simp
  rw [h1]
  rw [Set.ncard_coe_Finset]
  sorry

[Aaron Liu]

unfortunately Nat.digits is not reducible enough so decide doesn't work, I have a PR #25864 which fixes this

[Vlad]

n.digits 10 is the representation of number 10 in base n. The base 10 representation is Nat.digits 10 n. The theorem can be proved using native_decide, if that is acceptable.

example :
{n : ℕ | n ∈ Finset.Icc 1000 9999 ∧ Odd n ∧ (Nat.digits 10 n).Nodup}.ncard = 2240 := by
  rw [←Finset.coe_filter, Set.ncard_coe_finset]; native_decide