Skip to content

Comment on Verified dynamic programming with Σ-types in Leanparent

Comments

Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard

    Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x.
Then immediately I dropped that class. Turns out I like real analysis much more
AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.