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.

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

[Merged by Bors] - refactor: generalize SMul (Ideal R) (Submodule R M) to SMul (Submodule R A) (Submodule R M) #18419

Closed
wants to merge 32 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
94d510a
refactor: generalize mul of Submodule and smul of Ideal on Submodule …
alreadydone Oct 13, 2024
c31a232
Discard changes to Mathlib/RingTheory/JacobsonIdeal.lean
alreadydone Oct 13, 2024
71046e2
fixes
alreadydone Oct 13, 2024
fb0536c
fixes
alreadydone Oct 13, 2024
3cbb1e9
fixes
alreadydone Oct 14, 2024
810908a
fixes
alreadydone Oct 14, 2024
0c22392
fixes
alreadydone Oct 14, 2024
2af93ae
fixes
alreadydone Oct 14, 2024
e3e517d
missing docstring
alreadydone Oct 14, 2024
1fcc086
Merge branch 'master' into Ideal.mul
alreadydone Oct 18, 2024
913d508
Merge branch 'master' into Ideal.mul
alreadydone Oct 18, 2024
ff7e3bb
fixes
alreadydone Oct 18, 2024
74c5fbf
Merge branch 'master' into Ideal.mul
alreadydone Oct 24, 2024
b8032bc
Merge branch 'master' into Ideal.mul
alreadydone Oct 24, 2024
1751a4d
Merge branch 'master' into Ideal.mul
alreadydone Oct 26, 2024
54e02d4
fixes
alreadydone Oct 26, 2024
b6a7eb9
refactor: generalize AddSubmonoid Mul lemmas to SMul
alreadydone Oct 27, 2024
b0ba705
golf Ideal/Operations using the SMul lemmas
alreadydone Oct 27, 2024
62c1fa9
fix + minigolfs
alreadydone Oct 27, 2024
5e67fb1
minigolfs
alreadydone Oct 27, 2024
fe39874
get rid of large-import
alreadydone Oct 27, 2024
ff411cc
Merge branch 'master' into Ideal.mul
alreadydone Oct 28, 2024
9f9c59d
reduce diff
alreadydone Oct 28, 2024
97f5e9a
revert
alreadydone Oct 28, 2024
e5fd5d6
generalize to SMul (Submodule R A) (Submodule R M)
alreadydone Oct 29, 2024
46cd376
fix
alreadydone Oct 30, 2024
8cabc5f
fix
alreadydone Oct 30, 2024
5f8fc87
minor
alreadydone Oct 30, 2024
6546fad
Merge branch 'master' into Submodule.SMul
alreadydone Nov 8, 2024
09ec416
Merge pull request #19706 from leanprover-community/master
alreadydone Dec 3, 2024
d3c5b98
move lemma
alreadydone Dec 3, 2024
efe2593
Merge branch 'master' into Submodule.SMul
alreadydone Dec 4, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Merge branch 'master' into Ideal.mul
  • Loading branch information
alreadydone authored Oct 18, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 913d50834f011c1af1db4a638c1e4824de470e59

This merge commit was added into this branch cleanly.

There are no new changes to show, but you can still view the diff.