FoxDifferential/RightDerivative.lean
1import FoxDifferential.RightDerivative.GeometricSeries
2import FoxDifferential.RightDerivative.Basic
3import FoxDifferential.RightDerivative.Semidirect
4import FoxDifferential.RightDerivative.IntegerPower
5import FoxDifferential.RightDerivative.CommutatorFormula
7/-
8PUBLIC_PAGE_SNAPSHOT
9generated_at: 2026-05-27T09:47:29+09:00
10lean_source: lean4/FoxDifferential/RightDerivative.lean
11translation_root: data/translation
12purpose: identifies the local data snapshot used to build pages/
13placement: after imports, never before imports
14-/
15/-!
16# Right Fox derivatives
18Right crossed derivations of integral group rings, their semidirect-product model, integer-power
19formulas, and commutator formulas. This layer is independent of MPC and may be used by both
20Crowell and metabelian-product arguments.
21-/