Module

Coeff.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff

1 declaration indexed from sourceView source ↗

Module documentation

The principal declarations in this module are:

The prime-power moduli used throughout the compatibility layer are positive.

Imports1

Imported by3

theorem

FoxDifferential.primePower_pos

Documentation

The prime-power moduli used throughout the compatibility layer are positive.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u

Lean source · statement

theorem primePower_pos (ℓ a : ℕ) [Fact (0 < ℓ)] : 0 < ℓ ^ a