Def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?

Modification history

2023-09-08 09:40

Mathlib/Tactic/NormNum/CharZero.lean

chore: split Tactic.NormNum.Basic (#7002) …

Modified Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?View on Github →

2023-09-05 10:32

Mathlib/Tactic/NormNum/CharZero.lean

chore: minimize imports in NormNum.Core (#6953) …

Modified Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?View on Github →

2023-01-22 01:26

Mathlib/Tactic/NormNum/Core.lean

feat: `=`, `≠`, `<`, and `≤` functionality for `norm_num` (#1568) …

Added Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?View on Github →