[Merged by Bors] - feat(group_theory): simple lemmas for Wedderburn #18862
Conversation
ericrbg
added
awaiting-review
github-actions
bot
added
the
modifies-synchronized-file
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
| @@ -192,6 +192,8 @@ local attribute [instance] orbit_rel | |||
|
|
|||
| variables {α} {β} | |||
|
|
|||
| lemma orbit_rel_rel_iff {x y : β} : (orbit_rel α β).rel x y ↔ x ∈ orbit α y := iff.rfl | |||
There was a problem hiding this comment.
and yes, this new name is pretty terrible - suggestions welcome too here Yael
There was a problem hiding this comment.
orbit_rel_apply? But to make this name work we would need setoid α to be fun_like. Why isn't it already?
There was a problem hiding this comment.
this is not a refactor that should be done in lean3 :b I'll stick with that
There was a problem hiding this comment.
To be fair, you don't to refactor anything to add the instance. And you can make a simp lemma coe_eq_rel : ⇑s = s.rel to avoid needing to translate the API.
github-actions
bot
removed
the
awaiting-CI
src/group_theory/subgroup/basic.lean
Outdated
| @@ -2670,6 +2670,16 @@ begin | |||
| exact subset_normal_closure (set.mem_singleton _), | |||
| end | |||
|
|
|||
| variables (G) {M : Type*} [monoid M] | |||
|
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
These lemmas are a bit disparate, but they are all useful for Wedderburn's little theorem. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
These lemmas are a bit disparate, but they are all useful for Wedderburn's little theorem.