My homepage's puzzle

Changes

1 changed files (+17/-0)

• Homepage.lean (new)
  • @@ -0,0 +1,17 @@
    + import Mathlib + + open Equiv Finset Fintype Nat Quaternion Real + + instance : Coe Nat Char where + coe x := Char.ofNat x + + instance : Coe Char Nat where + coe x := x.toNat + + instance : Coe Int Nat where + coe x := x.toNat + + example : let _11:=minFac '⓫' + (·+97)<$>[0/0,_11,-(⟨1,0,2,4⟩:ℍ[ℤ])^2|>.re,2|>λo↦#{o∈Ioo o<|o<<<o|||o|o∣o},catalan 4,_11,(φ 5)!,↑((4:Fin 24)-6),floor<|deriv (sin ·^69) π,_11,card<|Perm<|Fin 3] = "anthonywang".toList := by + simp [minFac, minFacAux, catalan_eq_centralBinom_div] + decide