Skip to content

[Merged by Bors] - feat: basic structural lemmas about finite crystallographic root pairings.#21932

Closed
ocfnash wants to merge 2 commits intomasterfrom
ocfnash/rp_sub_mem
Closed

[Merged by Bors] - feat: basic structural lemmas about finite crystallographic root pairings.#21932
ocfnash wants to merge 2 commits intomasterfrom
ocfnash/rp_sub_mem

Conversation

@ocfnash
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash commented Feb 15, 2025

Open in Gitpod

@ocfnash ocfnash added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Feb 15, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 15, 2025 •
edited
Loading

PR summary 509488c0bf

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (new file) 1417

Declarations diff

+ coxeterWeightIn_eq_four_iff_not_linearIndependent
+ coxeterWeightIn_eq_zero_iff
+ divisorsAntidiagonal_four
+ divisorsAntidiagonal_one
+ divisorsAntidiagonal_three
+ divisorsAntidiagonal_two
+ instance [Finite ι] : Module.Finite R P.corootSpan := Finite.span_of_finite R <| finite_range _
+ instance [Finite ι] : Module.Finite R P.rootSpan := Finite.span_of_finite R <| finite_range _
+ linearIndependent_iff_coxeterWeightIn_ne_four
+ mul_mem_one_two_three_iff
+ mul_mem_zero_one_two_three_four_iff
+ neg_coroot_mem
+ neg_mem_range_coroot_iff
+ neg_mem_range_root_iff
+ neg_root_mem
+ pairingIn_neg_one_neg_four_iff
+ pairingIn_neg_two_neg_two_iff
+ pairingIn_one_four_iff
+ pairingIn_pairingIn_mem_set_of_isCrystallographic
+ pairingIn_reflection_perm_self_left
+ pairingIn_reflection_perm_self_right
+ pairingIn_two_two_iff
+ root_add_root_mem_of_pairingIn_neg
+ root_sub_root_mem_of_pairingIn_pos
- coxeterWeight_mem_set_of_isCrystallographic

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

@ocfnash ocfnash force-pushed the ocfnash/rp_sub_mem branch 2 times, most recently from f452e3e to ce7dffe Compare February 16, 2025 15:43
@ocfnash ocfnash mentioned this pull request Feb 16, 2025
Closed
@ocfnash ocfnash force-pushed the ocfnash/rp_sub_mem branch 2 times, most recently from 55dc2fb to 224461b Compare February 21, 2025 08:57
@ocfnash ocfnash removed the WIP Work in progress label Feb 21, 2025
ocfnash
ocfnash commented Feb 21, 2025
View reviewed changes
Mathlib/NumberTheory/Divisors.lean

@[simp] lemma divisorsAntidiag_zero : divisorsAntidiag 0 = ∅ := rfl

-- TODO Write a simproc instead of `divisorsAntidiagonal_one`, ..., `divisorsAntidiagonal_four` ...
Copy link
Copy Markdown
Contributor Author

@ocfnash ocfnash Feb 21, 2025

Choose a reason for hiding this comment

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

Such a simproc is probably incoming via #21915 but I'm hoping we do not need to be blocked on that.

(Of course I will happily wait if others feel we should.)

jcommelin
jcommelin reviewed Feb 21, 2025
View reviewed changes
Copy link
Copy Markdown
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.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 21, 2025

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

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 21, 2025
@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Feb 21, 2025

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 21, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 21, 2025
@ocfnash
feat: basic structural lemmas about finite crystallographic root pair…
8d0660f 
…ings. (#21932)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 21, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: basic structural lemmas about finite crystallographic root pairings. [Merged by Bors] - feat: basic structural lemmas about finite crystallographic root pairings. Feb 21, 2025
@mathlib-bors mathlib-bors bot closed this Feb 21, 2025
@mathlib-bors mathlib-bors bot deleted the ocfnash/rp_sub_mem branch February 21, 2025 22:20
Julian added a commit that referenced this pull request Feb 22, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
48af835 
* origin/master:
  chore(*): add `@[fun_prop]` (#22183)
  chore(RingTheory): generalize universes for `isUnramified_iff_map_eq` (#22185)
  chore(Algebra/GroupPower/IterateHom): move all lemmas earlier (#22132)
  feat(Probability): ae filter and integrability wrt a composition of kernel and measure (#22074)
  feat(CategoryTheory): forgetting the group structure on the codomain of left-exact functors (#21973)
  feat(CategoryTheory): embeddings for opposites of Grothendieck abelian categories (#22182)
  feat(CategoryTheory): `AsSmall C` is abelian (#22184)
  feat(CategoryTheory): explicit argument versions of `epi_comp` and `mono_comp` (#22181)
  feat(Topology/Instances/EReal/Lemmas): add lemmas about limsup and multiplication (#21833)
  feat: basic structural lemmas about finite crystallographic root pairings. (#21932)
  Rename `Mem𝓛p` to `MemLp` (#22164)
  feat(Logic/Equiv): Upgrade arrowProdEquivProdArrow to dependent types (#21518)
  feat(CategoryTheory): Grothendieck abelian categories have enough injectives (#20079)
  chore: deprecate Finite.cast_card_eq_mk (#22161)
  feat(CategoryTheory/Limits/Fubini): relax `HasLimits` hypotheses (#20570)
  chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up (#22109)
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

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

2 participants

@ocfnash @jcommelin