Commit 2024-12-20 12:30 486b7112

View on Github →

chore(GodelBetaFunction): use getElem (#20105)

Estimated changes

Modified Mathlib/Logic/Godel/GodelBetaFunction.lean

modified theorem Nat.beta_unbeta_coe