power of isomorphisms

Stream: mathlib4

[Kenny Lau]

(see correct examples below)

[Kenny Lau]

making it rfl would probably be a large refactor (so maybe only @Yaël Dillies would be qualified to do that), but maybe we can at least have a (simp) lemma?

[Yaël Dillies]

There was indeed a PR of mine somewhere doing exactly this

[Aaron Liu]

I don't think what you've written is actually true

[Aaron Liu]

pointwise power of ring hom not the same as iterating the ring hom

[Kenny Lau]

there's no structure on ring hom

[Kenny Lau]

adding two ring homs doesn't preserve multiplication, multiplying two ring homs doesn't preserve addition

[Aaron Liu]

So you want to add an instance for multiplying ringauts by composition?

[Kenny Lau]

it's already there

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Ring/Aut.html#RingAut.instGroup

[Kenny Lau]

ah you're right my statements should be ⇑(e ^ n) instead

[Kenny Lau]

import Mathlib

variable (R : Type*) [CommRing R]

#synth Group (R ≃+* R)
example (e : R ≃+* R) (n : ℕ) : ⇑(e ^ n) = e^[n] := rfl -- nope

example (e : R ≃+* R) (n : ℕ) : ⇑(e ^ n) = e^[n] :=
  n.recOn rfl fun _ ih ↦ congr($ih ∘ $rfl)

[Kenny Lau]

@Yaël Dillies can you link to your PR?

[Aaron Liu]

Kenny Lau said:

making it rfl would probably be a large refactor (so maybe only Yaël Dillies would be qualified to do that), but maybe we can at least have a (simp) lemma?

I think it would not be, what makes you think this is a big thing?

[Kenny Lau]

i don't know