Def Rat.rawCast

Modification history

2023-09-11 13:37

Mathlib/Tactic/NormNum/Core.lean

chore: further cleanup of `norm_num` (#7046) …

Modified Rat.rawCast View on Github →

2023-03-07 23:14

Mathlib/Tactic/NormNum/Core.lean

fix: to_additive issue with numerals in constant type family (#2419) …

Modified Rat.rawCast View on Github →

2023-01-27 15:48

Mathlib/Tactic/NormNum/Core.lean

feat: `Rat` functionality for `ring` (#1711) …

Added Rat.rawCast View on Github →