Commit 2023-05-06 12:10 38dbcd82

View on Github →

feat: enable cancel_denoms preprocessor in linarith (#3801) Enable the cancelDenoms preprocessor in linarith. Closes #2714.

depends on: #3797

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Analysis/Normed/Order/UpperLower.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Nat/Digits.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Expr.containsConst

added def Lean.Expr.rewrite

added def Lean.Expr.rewriteType

Modified Mathlib/Tactic/Linarith/Datatypes.lean

modified def Linarith.GlobalPreprocessor.branching

modified def Linarith.Preprocessor.globalize

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

added def Linarith.cancelDenoms

added def Linarith.normalizeDenominatorsLHS

added theorem Linarith.without_one_mul

Modified Mathlib/Topology/Homotopy/Basic.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/CantorScheme.lean

Modified Mathlib/Topology/PathConnected.lean

Modified Mathlib/Topology/UnitInterval.lean

Modified test/linarith.lean

added def P

deleted def R

added theorem T.works

Modified test/linear_combination.lean