FoxDifferential/RightDerivative/IntegerPower.lean
1import FoxDifferential.RightDerivative.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/RightDerivative/IntegerPower.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Right Fox derivatives
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20def signedGeomSeries {G : Type*} [Group G] (g : G) : ℤ → FoxDifferential.GroupRing G
21 | Int.ofNat n => geomSeries g n
22 | Int.negSucc n => -(MonoidAlgebra.of ℤ G g⁻¹ * geomSeries g⁻¹ (n + 1))
24namespace RightDerivation
26variable {G : Type*} [Group G]
28theorem map_zpow_groupElement (D : RightDerivation G) (g : G) :
29 ∀ n : ℤ,
30 D (MonoidAlgebra.of ℤ G (g ^ n) : FoxDifferential.GroupRing G) =
31 D (MonoidAlgebra.of ℤ G g : FoxDifferential.GroupRing G) * signedGeomSeries g n
32 | Int.ofNat n => by
33 simpa [signedGeomSeries] using D.map_pow_groupElement g n
34 | Int.negSucc n => by
35 have hpow := D.map_pow_groupElement g⁻¹ (n + 1)
36 rw [map_inv_groupElement] at hpow
37 simpa [signedGeomSeries, mul_assoc] using hpow
41end
43end FoxDifferential