zpow_succ

Stream: Is there code for X?

[Kim Morrison]

Where is

import Mathlib

theorem zpow_succ {G : Type} [Group G] (g : G) (x : Int) : g ^ (x + 1) = g * g ^ x := sorry

[Kim Morrison]

ugh, (mul_self_zpow g x).symm, okay

[Kim Morrison]

Seems weird to be missing this?

[Jireh Loreaux]

A little, but succ is slightly weird terminology to use for Int, right? I know we have docs#Int.succ, but I mean that we would normally use add_one.

[Kim Morrison]

Sure, zpow_add_one is fine.

[Johan Commelin]

I guess that lemma isn't very confluent with zpow_add? Should the RHS by g ^ x * g?

[Yaël Dillies]

Sorry, have you missed docs#zpow_add_one ?

[Kim Morrison]

Yes! :-)

[Jireh Loreaux]

Lol, I feel justified.