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(group_theory/order_of_element): now makes sense for infinite monoids #6587

Closed
wants to merge 40 commits into from
Closed
Changes from 5 commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
8399983
refactored the definition of order_of
Julian-Kuelshammer Mar 8, 2021
0ca3dd3
some minor changes
Julian-Kuelshammer Mar 8, 2021
bbb754f
style
Julian-Kuelshammer Mar 8, 2021
bf02842
Apply suggestions from code review
Julian-Kuelshammer Mar 8, 2021
bd223ee
moved instance and corrected typos
Julian-Kuelshammer Mar 8, 2021
f11c5a2
some fun with decidable
Julian-Kuelshammer Mar 9, 2021
4300b0b
some more decidable changes
Julian-Kuelshammer Mar 9, 2021
23b4556
some linting
Julian-Kuelshammer Mar 9, 2021
394cf44
fix broken `simp`
eric-wieser Mar 9, 2021
f6aabe8
some more fixes
Julian-Kuelshammer Mar 9, 2021
314e8b2
fixing decidable_gpowers
Julian-Kuelshammer Mar 9, 2021
7b3d2da
remove some double group structures
Julian-Kuelshammer Mar 9, 2021
45aebc4
100 linter
Julian-Kuelshammer Mar 9, 2021
2288e1f
main file compiles again
Julian-Kuelshammer Mar 10, 2021
d85c3b0
clean up duplicate group arguments
Julian-Kuelshammer Mar 10, 2021
898af1a
had to add a classical
Julian-Kuelshammer Mar 10, 2021
38d2a20
reestablished order_of_pos
Julian-Kuelshammer Mar 10, 2021
e06be08
reestablished order_of_pow
Julian-Kuelshammer Mar 10, 2021
c6e0770
line linter
Julian-Kuelshammer Mar 10, 2021
15ce8ca
fix of perm
Julian-Kuelshammer Mar 10, 2021
7ad74fe
let's not get that constructive
Julian-Kuelshammer Mar 10, 2021
d03484a
some linting
Julian-Kuelshammer Mar 10, 2021
43c4c04
fix char_p
Julian-Kuelshammer Mar 10, 2021
0a1de4a
fixed integral_domain
Julian-Kuelshammer Mar 10, 2021
2c29043
going back to classical
Julian-Kuelshammer Mar 11, 2021
7508b10
some cleanup
Julian-Kuelshammer Mar 11, 2021
76bf6fe
more cleanup
Julian-Kuelshammer Mar 11, 2021
d0554c2
more cleanup
Julian-Kuelshammer Mar 11, 2021
ea1d1c1
some generalisations
Julian-Kuelshammer Mar 11, 2021
7584e61
some fixes
Julian-Kuelshammer Mar 11, 2021
9ad5bb5
dihedral
Julian-Kuelshammer Mar 12, 2021
b8c9de4
more dihedral
Julian-Kuelshammer Mar 12, 2021
f0df477
line linter
Julian-Kuelshammer Mar 12, 2021
6bb7bb6
one thing fixed
Julian-Kuelshammer Mar 12, 2021
657f961
appearently it was a universe issue
Julian-Kuelshammer Mar 12, 2021
f0c856f
modify documentation
Julian-Kuelshammer Mar 13, 2021
d5261c8
git merge master
Julian-Kuelshammer Mar 15, 2021
2d030b6
Apply suggestions from code review
Julian-Kuelshammer Mar 16, 2021
317fe9d
added warning about multiplicativity
Julian-Kuelshammer Mar 16, 2021
00f0174
indentation
Julian-Kuelshammer Mar 16, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view