NYLL
Module

Additive.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive
16 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — prime-power augmentation ideal — additive

The principal declarations in this module are:

  • instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage

Each finite-stage prime-power augmentation ideal inherits an additive commutative group structure from its ambient finite group algebra.

  • instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily

The dependent family of finite-stage prime-power augmentation ideals carries the pointwise additive commutative group structure.

  • coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal

The inclusion of the completed augmentation ideal preserves zero.

  • coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal

The inclusion of the completed augmentation ideal preserves addition.

Imports1
Imported by2

Declarations

instance

instZeroPrimePowerCompletedGroupAlgebraAugmentationIdeal

L42 ↗
FoxDifferential.instZeroPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The zero element of the prime-power completed augmentation ideal is the compatible family of zero elements at all finite stages.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instZeroPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    Zero (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  zero := ⟨fun i =>
    (0 : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i), by
    intro i j hij
    apply Subtype.ext
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
      (0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
    exact map_zero _⟩
instance

instAddPrimePowerCompletedGroupAlgebraAugmentationIdeal

L56 ↗
FoxDifferential.instAddPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

Addition in the prime-power completed augmentation ideal is defined coordinatewise through finite stages.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    Add (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  add x y := ⟨fun i =>
      (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
        from x.1 i) +
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from y.1 i), by
    intro i j hij
    apply Subtype.ext
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j) +
          ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) =
      (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
        ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
    rw [map_add]
    exact congrArg₂ HAdd.hAdd
      (congrArg Subtype.val (x.2 i j hij))
      (congrArg Subtype.val (y.2 i j hij))⟩
instance

instAddZeroClassPrimePowerCompletedGroupAlgebraAugmentationIdeal

L83 ↗
FoxDifferential.instAddZeroClassPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

Coordinatewise zero and addition on the prime-power completed augmentation ideal satisfy the left and right zero laws.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddZeroClassPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    AddZeroClass (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext i
    apply Subtype.ext
    change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
      ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
        PrimePowerCompletedGroupAlgebraStage ℓ G i) =
      ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
        PrimePowerCompletedGroupAlgebraStage ℓ G i)
    simp only [zero_add]
  add_zero x := by
    apply Subtype.ext
    funext i
    apply Subtype.ext
    change ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal
        (ℓ := ℓ) (G := G) i from x.1 i) :
        PrimePowerCompletedGroupAlgebraStage ℓ G i) +
      (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
      ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
        PrimePowerCompletedGroupAlgebraStage ℓ G i)
    simp only [add_zero]
instance

instNegPrimePowerCompletedGroupAlgebraAugmentationIdeal

L113 ↗
FoxDifferential.instNegPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

Negation on the prime-power completed augmentation ideal is defined coordinatewise through finite-stage negations.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instNegPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    Neg (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  neg x := ⟨fun i =>
    -(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
      from x.1 i), by
    intro i j hij
    apply Subtype.ext
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (-(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
      -(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
    rw [map_neg]
    exact congrArg Neg.neg (congrArg Subtype.val (x.2 i j hij))⟩
instance

instSubPrimePowerCompletedGroupAlgebraAugmentationIdeal

L132 ↗
FoxDifferential.instSubPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

Subtraction on the prime-power completed augmentation ideal is defined coordinatewise through the finite-stage augmentation ideals.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSubPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    Sub (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  sub x y := ⟨fun i =>
      (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
        from x.1 i) -
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from y.1 i), by
    intro i j hij
    apply Subtype.ext
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        ((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) -
          (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
      ((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
            from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)) -
        (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
            from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)))
    rw [map_sub]
    exact congrArg₂ HSub.hSub
      (congrArg Subtype.val (x.2 i j hij))
      (congrArg Subtype.val (y.2 i j hij))⟩
instance

instSMulNatPrimePowerCompletedGroupAlgebraAugmentationIdeal

L159 ↗
FoxDifferential.instSMulNatPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The prime-power completed augmentation ideal carries natural-number scalar multiplication coordinatewise at every finite quotient stage.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSMulNatPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    SMul ℕ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  smul m x := ⟨fun i =>
    m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
      from x.1 i), by
    intro i j hij
    apply Subtype.ext
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
      m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
    rw [map_nsmul]
    exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩
instance

instSMulIntPrimePowerCompletedGroupAlgebraAugmentationIdeal

L178 ↗
FoxDifferential.instSMulIntPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The prime-power completed augmentation ideal carries integer scalar multiplication coordinatewise at every finite quotient stage.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSMulIntPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    SMul ℤ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  smul m x := ⟨fun i =>
    m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
      from x.1 i), by
    intro i j hij
    apply Subtype.ext
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
      m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
          from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
    rw [map_zsmul]
    exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩
def

instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage

L198 ↗
FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
Documentation

Each finite-stage prime-power augmentation ideal inherits an additive commutative group structure from its ambient finite group algebra.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    AddCommGroup ((primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i)
def

instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily

L210 ↗
FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
Documentation

The dependent family of finite-stage prime-power augmentation ideals carries the pointwise additive commutative group structure.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
Lean source · statement
def instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily :
    AddCommGroup
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i)
theorem

coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal

L220 ↗
FoxDifferential.coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inclusion of the completed augmentation ideal preserves zero.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal :
    ((0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = 0
theorem

coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal

L230 ↗
FoxDifferential.coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inclusion of the completed augmentation ideal preserves addition.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal
    (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    ((x + y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x + y
theorem

coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal

L241 ↗
FoxDifferential.coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inclusion of the completed augmentation ideal preserves negation.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    ((-x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = -x
theorem

coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal

L252 ↗
FoxDifferential.coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inclusion of the completed augmentation ideal preserves subtraction.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal
    (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    ((x - y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x - y
theorem

coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal

L266 ↗
FoxDifferential.coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inclusion of the completed augmentation ideal preserves natural-number scalar multiplication.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    ((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • x
theorem

coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal

L277 ↗
FoxDifferential.coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inclusion of the completed augmentation ideal preserves integer scalar multiplication.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    ((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • x
instance

instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdeal

L289 ↗
FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The prime-power completed augmentation ideal inherits an additive commutative group structure from its injective inclusion into the family of finite-stage ideals.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
Lean source · statement
instance instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    AddCommGroup (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.