Commit 2023-01-14 05:03 24122eed

View on Github →

fix: sorries in Tactic.NormNum.Core (#1564)

Estimated changes

Modified Mathlib/Algebra/Invertible.lean

deleted theorem Invertible.cong

added theorem Invertible.congr

Modified Mathlib/Tactic/NormNum/Core.lean

deleted theorem Mathlib.Meta.NormNum.IsRat.of_raw

modified theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq

deleted def Mathlib.Meta.NormNum.Result.ofRawRat