Skip to content

Instantly share code, notes, and snippets.

/- https://leanprover-community.github.io/lean-web-editor -/
import data.real.basic
import init.classical
import algebra.invertible
import algebra.euclidean_domain
import tactic.ring_exp
/- Problem: Find all functions satisfying `prop` -/
def prop (f : ℝ → ℝ) : Prop :=