Use fancier notation for ceil

Changes

1 changed files (+1/-1)

• Homepage.lean
  • @@ -12,6 +12,6 @@ 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 + (·+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 simp [minFac, minFacAux, catalan_eq_centralBinom_div] decide