Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: cleanup more erw #20601

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore: cleanup more erw #20601

wants to merge 3 commits into from

Conversation

kim-em
Copy link
Contributor

@kim-em kim-em commented Jan 9, 2025

Open in Gitpod

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 9, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 9, 2025 •
edited
Loading

PR summary 854f114e6d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ subsemiringMap_apply_coe
+ subsemiringMap_symm_apply_coe

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.

Decrease in tech debt: (relative, absolute) = (1.86, 0.01)
Current number Change Type
203 -1 disabled simpNF lints
1448 -8 erw

Current commit 854f114e6d
Reference commit d4891b46ec

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).

@grunweg
Copy link
Collaborator

grunweg commented Jan 9, 2025

Can you fix the build, please?

@jcommelin
Copy link
Member

There is a whole directory DownStreamTest that I don't think you intended to add to this PR.

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 10, 2025
@kim-em kim-em removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 10, 2025
@kim-em
Copy link
Contributor Author

kim-em commented Jan 10, 2025

There is a whole directory DownStreamTest that I don't think you intended to add to this PR.

Fixed, thanks.

jcommelin
jcommelin reviewed Jan 10, 2025
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 10, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 10, 2025
@kim-em
chore: cleanup more erw (#20601)
220e307
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: cleanup more erw [Merged by Bors] - chore: cleanup more erw Jan 10, 2025
@mathlib-bors mathlib-bors bot closed this Jan 10, 2025
@mathlib-bors mathlib-bors bot deleted the more_erw2 branch January 10, 2025 07:43
grunweg pushed a commit that referenced this pull request Jan 11, 2025
@kim-em @grunweg
chore: cleanup more erw (#20601)
cb7915f
Julian added a commit that referenced this pull request Jan 12, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
9ba6079 
* origin/master: (88 commits)
  chore(scripts): update nolints.json (#20672)
  chore: de-simp `map_eq_zero_iff_eq_one` (#20662)
  feat(Combinatorics/SimpleGraph): add independent sets (#18608)
  chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641)
  feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366)
  feat(AlgebraicTopology): model categories (#19158)
  chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548)
  feat(Data/List/ReduceOption): add replicate theorems (#20644)
  feat: approximate subgroups (#20050)
  feat: use scoped trace nodes in linarith (#19855)
  feat: disjoint union of charted spaces (#20619)
  feat: add some term elaborators for reduction (#15192)
  feat(Topology/Category): category of delta-generated spaces (#19499)
  add a variable_alias for Quantale and AddQuantale (#19282)
  feat(Computability/DFA): implement `isRegular_iff` (#19940)
  chore: unpin and bump batteries and importgraph (#20651)
  chore: split `Mathlib/Algebra/Group/Int` (#20624)
  feat: three lemmas related to Hausdorff distance (#20585)
  chore: `initialize_simps_projections` for `Submodule` (#20582)
  feat(Order): Boolean algebra structure on idempotents (#20618)
  chore(CategoryTheory): moving/renaming Subpresheaf (#20583)
  refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630)
  feat: sets of doubling strictly less than 3/2 (#20572)
  chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452)
  feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298)
  feat: product of subalgebras (#20202)
  feat: `Submodule.restrictScalars` commutes with `pow` (#20581)
  feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580)
  chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576)
  chore: use ofNat more (#20546)
  feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363)
  feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797)
  refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590)
  feat: Make `PNat.recOn` induction eliminator (#20617)
  feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608)
  feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574)
  feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573)
  chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611)
  feat: AbsoluteValue.IsNontrivial (#20588)
  chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092)
  chore(Data/Set): split the `CoeSort` instance to its own file (#19031)
  feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612)
  feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286)
  chore: cleanup more `erw` (#20601)
  chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587)
  chore: cleanup imports in PrimePow/Divisors (#20626)
  chore: split Algebra/BigOperators/Group/List (#20625)
  chore: reduce Topology->Order imports by moving content (#20627)
  chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592)
  refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kim-em @grunweg @jcommelin @leanprover-community-mathlib4-bot