Commit 2024-01-11 14:47 2f63d25e

View on Github →

fix: patch for std4#198 (more mul lemmas for Nat) (#6204)

Estimated changes

Modified Mathlib/Algebra/EuclideanDomain/Instances.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

modified theorem SzemerediRegularity.le_stepBound

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/Nat/Choose/Central.lean

Modified Mathlib/Data/Nat/Defs.lean

Modified Mathlib/Data/Nat/Factorial/Basic.lean

Modified Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

Modified Mathlib/Data/Nat/Fib/Basic.lean

Modified Mathlib/Data/Nat/Order/Basic.lean

deleted theorem Nat.le_mul_of_pos_left

deleted theorem Nat.le_mul_of_pos_right

Modified Mathlib/Data/Nat/Sqrt.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem Eq.congr_left

deleted theorem Eq.congr_right

deleted theorem cast_cast

deleted theorem cast_eq_iff_heq

deleted theorem congr_fun₂

deleted theorem congr_fun₃

deleted theorem eq_mp_eq_cast

deleted theorem eq_mpr_eq_cast

deleted theorem funext₂

deleted theorem funext₃

deleted theorem heq_of_cast_eq

deleted theorem ne_of_apply_ne

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/FermatPsp.lean

Modified Mathlib/Tactic/NormNum/LegendreSymbol.lean

Modified lake-manifest.json

Modified test/apply_rules.lean