[Merged by Bors] - feat(Slope): slope_pos_iff_of_le and related lemmas by ChrisHughes24 · Pull Request #28039 · leanprover-community/mathlib4

ChrisHughes24 · 2025-08-06T13:07:29Z

github-actions · 2025-08-06T13:08:41Z

PR summary 5b83500e0e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ slope_eq_zero_iff
+ slope_neg_iff_of_le
+ slope_nonneg_iff_of_le
+ slope_nonpos_iff_of_le
+ slope_pos_iff_of_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/LinearAlgebra/AffineSpace/Slope.lean

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

…into slope_pos

Mathlib/LinearAlgebra/AffineSpace/Slope.lean

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Ruben-VandeVelde

Thanks!

maintainer merge

github-actions · 2025-08-14T14:50:52Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

riccardobrasca

Thanks!

bors d+

riccardobrasca · 2025-08-14T18:16:22Z

Mathlib/LinearAlgebra/AffineSpace/Slope.lean

  ext x y; exact slope_neg f x y

+lemma slope_eq_zero_iff {f : k → E} {a b : k} : slope f a b = 0 ↔ f a = f b := by
+  simp only [slope, vsub_eq_sub, smul_eq_zero, inv_eq_zero, sub_eq_zero, eq_comm,


Can you please use simp instead of simp only?

mathlib-bors · 2025-08-14T18:16:29Z

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

ChrisHughes24 · 2025-08-14T23:37:24Z

bors r+

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

mathlib-bors · 2025-08-15T00:30:47Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

…nity#28039) Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

feat(Slope): slope_pos_iff_of_le and related lemmas

e42a784

ChrisHughes24 mentioned this pull request Aug 6, 2025

feat(Calculus): exists_gt_of_deriv_pos and variants #27824

Open

1 task

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Aug 6, 2025

ChrisHughes24 added 2 commits August 6, 2025 14:23

golf

79275c4

generalize slope lemmas

bc3fb3c

themathqueen reviewed Aug 6, 2025

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Slope.lean Outdated Show resolved Hide resolved

ChrisHughes24 and others added 3 commits August 6, 2025 15:27

Update Mathlib/LinearAlgebra/AffineSpace/Slope.lean

1711a52

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

golf

6bc8413

Merge branch 'slope_pos' of https://github.com/ChrisHughes24/mathlib4 …

5ccc97f

…into slope_pos

themathqueen reviewed Aug 6, 2025

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Slope.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/AffineSpace/Slope.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

41b0b54

Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

Ruben-VandeVelde approved these changes Aug 14, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 14, 2025

riccardobrasca reviewed Aug 14, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 14, 2025

changes from comments

c5d7d04

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

feat(Slope): slope_pos_iff_of_le and related lemmas (#28039)

0c784d7

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

mathlib-bors bot changed the title ~~feat(Slope): slope_pos_iff_of_le and related lemmas~~ [Merged by Bors] - feat(Slope): slope_pos_iff_of_le and related lemmas Aug 15, 2025

mathlib-bors bot closed this Aug 15, 2025

Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025

feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-commu…

a8d8e35

…nity#28039) Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025

feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-commu…

2e9e813

…nity#28039) Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Slope): slope_pos_iff_of_le and related lemmas#28039

[Merged by Bors] - feat(Slope): slope_pos_iff_of_le and related lemmas#28039
ChrisHughes24 wants to merge 8 commits intoleanprover-community:masterfrom
ChrisHughes24:slope_pos

ChrisHughes24 commented Aug 6, 2025

Uh oh!

github-actions bot commented Aug 6, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Uh oh!

github-actions bot commented Aug 14, 2025

Uh oh!

riccardobrasca left a comment

Uh oh!

riccardobrasca Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

ChrisHughes24 commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

ChrisHughes24 commented Aug 6, 2025

Uh oh!

github-actions bot commented Aug 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5b83500e0e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 14, 2025

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Aug 14, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

ChrisHughes24 commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Aug 6, 2025 •

edited

Loading