φ monster

Changes

1 changed files (+3/-1)

• Homepage.lean
  • @@ -11,7 +11,9 @@ instance : Coe Char Nat where
    instance : Coe Int Nat where coe x := x.toNat + set_option maxRecDepth 1000 + 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),⌈deriv (sin ·^69) π⌉₊,_11,card<|Perm<|Fin 3] = "anthonywang".toList := by + (·+97)<$>[0/0,_11,-(⟨1,0,2,4⟩:ℍ[ℤ])^2|>.re,2|>λo↦#{o∈Ioo o<|o<<<o|||o|o∣o},catalan 4,_11,(φ∘φ∘φ∘φ∘φ∘φ<|4‼‼)!,↑((4:Fin 24)-6),⌈deriv (sin ·^69) π⌉₊,_11,card<|Perm<|Fin 3] = "anthonywang".toList := by simp [minFac, minFacAux, catalan_eq_centralBinom_div] decide