Commit 2024-10-15 16:48 a5f83b52

View on Github →

chore: split off Rat-based functions from Mathlib.Lean.Expr.Basic (#17778) Basic functions for working with expressions don't need to know about the rational numbers. (I checked this manually since assert_not_exists ins't imported here yet!)

Estimated changes