[Merged by Bors] - feat: port Algebra.Hom.Iterate
#1133
Conversation
winstonyin
added
awaiting-review
Mathlib/Algebra/Hom/Iterate.lean
Outdated
| theorem smul_iterate [MulAction G H] : ((· • ·) a : H → H)^[n] = (· • ·) (a ^ n) := | ||
| funext fun b => | ||
| Nat.recOn n (by dsimp only; rw [iterate_zero, id.def, pow_zero, one_smul G b]) | ||
| fun n ih => by dsimp only; rw [iterate_succ', comp_apply, ih, pow_succ, mul_smul] |
There was a problem hiding this comment.
Need dsimp only before rw works. This is happening quite frequently.
Mathlib/Algebra/Hom/Iterate.lean
Outdated
| variable [Monoid G] (a : G) (n : ℕ) | ||
|
|
||
| @[simp, to_additive] | ||
| theorem smul_iterate [MulAction G H] : ((· • ·) a : H → H)^[n] = (· • ·) (a ^ n) := |
There was a problem hiding this comment.
(· • ·) a is not a faithful port of (•) a which means Smul.smul a
There was a problem hiding this comment.
Would you recommend (· • ·) a or Smul.smul a during port?
There was a problem hiding this comment.
I've changed them to (a • ·) or (a * ·)
|
I've just added all the #aligns which to_additive doesn't generate. If anyone knows how to make leanprover-community/mathport#209 happen sooner, that would be great! |
| variable [Semigroup G] {a b c : G} | ||
|
|
||
| -- Porting note: need `dsimp only`, see https://leanprover.zulipchat.com/#narrow/stream/ | ||
| -- 287929-mathlib4/topic/dsimp.20before.20rw/near/317063489 |
There was a problem hiding this comment.
Yeah, the issue is https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/dsimp.20before.20rw/near/317064195 : (a * ·) t expands to (fun x ↦ a * x) t in lean 4, but ((*)a) t expands to a * t in lean 3, meaning that sometimes you have to dsimp only in Lean 4 to get back on track. You could mention this in the porting note but that's what's going on.
semorrison
added
ready-to-merge
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
Algebra.Hom.IterateAlgebra.Hom.Iterate
No description provided.