Commit 2023-08-28 21:38 a8ca8271

View on Github →

feat: use the function to help elaborate the injectivity lemma in apply_fun (#6733)

Estimated changes

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/Tactic/ApplyFun.lean

modified def Mathlib.Tactic.applyFunHyp

modified def Mathlib.Tactic.applyFunTarget

Modified test/apply_fun.lean