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] - feat(group_theory/perm/basic): mul_left
is a monoid hom
#17900
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here are a few difficulties I encountered.
|
||
import logic.function.iterate | ||
import group_theory.perm.basic | ||
import algebra.group_power.lemmas |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
algebra.hom.iterate
and group_theory.perm.basic
are neighbor files. It makes more sense to have equiv.perm.coe_pow
in group_theory.perm.basic
and I have an upcoming PR that will make it refl, so algebra.hom.iterate
won't even be needed anymore!
src/group_theory/perm/basic.lean
Outdated
section add_group | ||
variables [add_group α] (a b : α) | ||
|
||
@[simp] lemma add_left_zero : equiv.add_left (0 : α) = 1 := ext zero_add | ||
@[simp] lemma add_right_zero : equiv.add_right (0 : α) = 1 := ext add_zero | ||
|
||
@[simp] lemma add_left_add : equiv.add_left (a + b) = equiv.add_left a * equiv.add_left b := | ||
ext $ add_assoc _ _ | ||
|
||
@[simp] lemma add_right_add : equiv.add_right (a + b) = equiv.add_right b * equiv.add_right a := | ||
ext $ λ _, (add_assoc _ _ _).symm | ||
|
||
@[simp] lemma add_left_neg : equiv.add_left (-a) = (equiv.add_left a)⁻¹ := equiv.coe_inj.1 rfl | ||
@[simp] lemma add_right_neg : equiv.add_right (-a) = (equiv.add_right a)⁻¹ := equiv.coe_inj.1 rfl | ||
|
||
@[simp] lemma add_left_nsmul (n : ℕ) : equiv.add_left (n • a) = equiv.add_left a ^ n := | ||
map_nsmul (⟨equiv.add_left, add_left_zero, add_left_add⟩ : α →+ additive (perm α)) _ _ | ||
|
||
@[simp] lemma add_right_nsmul (n : ℕ) : equiv.add_right (n • a) = equiv.add_right a ^ n := | ||
@add_left_nsmul αᵃᵒᵖ _ _ _ | ||
|
||
@[simp] lemma add_left_zsmul (n : ℤ) : equiv.add_left (n • a) = equiv.add_left a ^ n := | ||
map_zsmul (⟨equiv.add_left, add_left_zero, add_left_add⟩ : α →+ additive (perm α)) _ _ | ||
|
||
@[simp] lemma add_right_zsmul (n : ℤ) : equiv.add_right (n • a) = equiv.add_right a ^ n := | ||
@add_left_zsmul αᵃᵒᵖ _ _ _ | ||
|
||
end add_group |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
to_additive
gave up on me throughout, because perm α
is a multiplicative group and to_additive
isn't smart enough to insert additive
in the right places.
src/group_theory/perm/basic.lean
Outdated
@[simp, to_additive] lemma mul_right_zpow : ∀ n : ℤ, equiv.mul_right (a ^ n) = equiv.mul_right a ^ n | ||
| (int.of_nat n) := by simp | ||
| (int.neg_succ_of_nat n) := by simp |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unexplicably, not a single proof works for the four of mul_left_pow
/mul_right_pow
/mul_left_zpow
/mul_right_zpow
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please don't forget to open a corresponding mathlib4 PR. LGTM otherwise.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib4 approved, so bors merge |
`equiv.mul_left` is a monoid homomorphism.
Pull request successfully merged into master. Build succeeded: |
mul_left
is a monoid hommul_left
is a monoid hom
equiv.mul_left
is a monoid homomorphism.Match leanprover-community/mathlib4#1348