Theorem Linarith.without_one_mul

Modification history

2024-07-16 20:24

Mathlib/Tactic/Linarith/Preprocessing.lean

chore(Tactic): reduce autoImplicit, part 4 (#14805) …

Modified Linarith.without_one_mul View on Github →

2023-05-06 12:10

Mathlib/Tactic/Linarith/Preprocessing.lean

feat: enable cancel_denoms preprocessor in linarith (#3801) …

Added Linarith.without_one_mul View on Github →