NYLL
Module

AddCommGroup.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup
20 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — in class — add

comm group

The principal declarations in this module are:

  • coe_zero_modNCompletedGroupAlgebraInClass

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero.

  • coe_add_modNCompletedGroupAlgebraInClass

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition.

  • coe_neg_modNCompletedGroupAlgebraInClass

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves negation.

  • coe_sub_modNCompletedGroupAlgebraInClass

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves subtraction.

Imports1
Imported by1

Declarations

instance

instZeroModNCompletedGroupAlgebraInClass

L45 ↗
FoxDifferential.instZeroModNCompletedGroupAlgebraInClass
Documentation

The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instZeroModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Zero (ModNCompletedGroupAlgebraInClass n G C) where
  zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStageInClass n G C U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
      (0 : ModNCompletedGroupAlgebraStageInClass n G C V) = 0
    exact map_zero _⟩
instance

instAddModNCompletedGroupAlgebraInClass

L58 ↗
FoxDifferential.instAddModNCompletedGroupAlgebraInClass
Documentation

Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Add (ModNCompletedGroupAlgebraInClass n G C) where
  add x y := ⟨fun U =>
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
        (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
    intro U V hUV
    calc
      modNCompletedGroupAlgebraTransitionInClass n G C hUV
          ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
            (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V))
        =
          modNCompletedGroupAlgebraTransitionInClass n G C hUV
            (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
          modNCompletedGroupAlgebraTransitionInClass n G C hUV
            (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V) := by
            rw [map_add]
      _ =
          (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
            (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U) := by
            exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩
instance

instAddZeroClassModNCompletedGroupAlgebraInClass

L84 ↗
FoxDifferential.instAddZeroClassModNCompletedGroupAlgebraInClass
Documentation

Coordinatewise zero and addition on the class-indexed mod-\(n\) completed group algebra satisfy the left and right zero laws.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddZeroClassModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    AddZeroClass (ModNCompletedGroupAlgebraInClass n G C) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext U
    change (0 : ModNCompletedGroupAlgebraStageInClass n G C U) +
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) =
        (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    simp only [zero_add]
  add_zero x := by
    apply Subtype.ext
    funext U
    change (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
      (0 : ModNCompletedGroupAlgebraStageInClass n G C U) =
        (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    simp only [add_zero]
instance

instNegModNCompletedGroupAlgebraInClass

L108 ↗
FoxDifferential.instNegModNCompletedGroupAlgebraInClass
Documentation

Negation on the \(C\)-indexed mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra negations.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instNegModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Neg (ModNCompletedGroupAlgebraInClass n G C) where
  neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (-(show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
      -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 U V hUV)⟩
instance

instSubModNCompletedGroupAlgebraInClass

L123 ↗
FoxDifferential.instSubModNCompletedGroupAlgebraInClass
Documentation

Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSubModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Sub (ModNCompletedGroupAlgebraInClass n G C) where
  sub x y := ⟨fun U =>
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
        (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) -
          (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V)) =
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
        (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩
instance

instSMulNatModNCompletedGroupAlgebraInClass

L142 ↗
FoxDifferential.instSMulNatModNCompletedGroupAlgebraInClass
Documentation

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSMulNatModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    SMul ℕ (ModNCompletedGroupAlgebraInClass n G C) where
  smul m x := ⟨fun U =>
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 U V hUV)⟩
instance

instSMulIntModNCompletedGroupAlgebraInClass

L158 ↗
FoxDifferential.instSMulIntModNCompletedGroupAlgebraInClass
Documentation

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSMulIntModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    SMul ℤ (ModNCompletedGroupAlgebraInClass n G C) where
  smul m x := ⟨fun U =>
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 U V hUV)⟩
theorem

coe_zero_modNCompletedGroupAlgebraInClass

L176 ↗
FoxDifferential.coe_zero_modNCompletedGroupAlgebraInClass
Documentation

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_zero_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    ((0 : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = 0
theorem

coe_add_modNCompletedGroupAlgebraInClass

L190 ↗
FoxDifferential.coe_add_modNCompletedGroupAlgebraInClass
Documentation

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_add_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    ((x + y : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = x + y
theorem

coe_neg_modNCompletedGroupAlgebraInClass

L205 ↗
FoxDifferential.coe_neg_modNCompletedGroupAlgebraInClass
Documentation

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves negation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_neg_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ModNCompletedGroupAlgebraInClass n G C) :
    ((-x : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = -x
theorem

coe_sub_modNCompletedGroupAlgebraInClass

L220 ↗
FoxDifferential.coe_sub_modNCompletedGroupAlgebraInClass
Documentation

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves subtraction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_sub_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    ((x - y : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = x - y
theorem

coe_nsmul_modNCompletedGroupAlgebraInClass

L235 ↗
FoxDifferential.coe_nsmul_modNCompletedGroupAlgebraInClass
Documentation

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves natural-number scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_nsmul_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    ((m • x : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = m • x
theorem

coe_zsmul_modNCompletedGroupAlgebraInClass

L250 ↗
FoxDifferential.coe_zsmul_modNCompletedGroupAlgebraInClass
Documentation

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves integer scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem coe_zsmul_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    ((m • x : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = m • x
instance

instAddCommGroupModNCompletedGroupAlgebraInClass

L263 ↗
FoxDifferential.instAddCommGroupModNCompletedGroupAlgebraInClass
Documentation

The class-indexed mod-\(n\) completion inherits an additive commutative group structure from its injective inclusion into the family of finite stages.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instAddCommGroupModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    AddCommGroup (ModNCompletedGroupAlgebraInClass n G C)
theorem

modNCompletedGroupAlgebraProjectionInClass_zero

L282 ↗
FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_zero
Documentation

The finite-stage projection sends \(0\) to \(0\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjectionInClass_zero
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U
      (0 : ModNCompletedGroupAlgebraInClass n G C) = 0
theorem

modNCompletedGroupAlgebraProjectionInClass_add

L291 ↗
FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_add
Documentation

The mod-\(n\) finite-stage projection preserves addition.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjectionInClass_add
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (x + y) =
      modNCompletedGroupAlgebraProjectionInClass n G C U x +
        modNCompletedGroupAlgebraProjectionInClass n G C U y
theorem

modNCompletedGroupAlgebraProjectionInClass_neg

L302 ↗
FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_neg
Documentation

The mod-\(n\) finite-stage projection preserves negation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjectionInClass_neg
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (-x) =
      -modNCompletedGroupAlgebraProjectionInClass n G C U x
theorem

modNCompletedGroupAlgebraProjectionInClass_sub

L312 ↗
FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_sub
Documentation

The mod-\(n\) finite-stage projection preserves subtraction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjectionInClass_sub
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (x - y) =
      modNCompletedGroupAlgebraProjectionInClass n G C U x -
        modNCompletedGroupAlgebraProjectionInClass n G C U y
theorem

modNCompletedGroupAlgebraProjectionInClass_nsmul

L323 ↗
FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_nsmul
Documentation

The finite-stage projection is compatible with natural-number scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjectionInClass_nsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
      m • modNCompletedGroupAlgebraProjectionInClass n G C U x
theorem

modNCompletedGroupAlgebraProjectionInClass_zsmul

L333 ↗
FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_zsmul
Documentation

The finite-stage projection is compatible with integer scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjectionInClass_zsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
      m • modNCompletedGroupAlgebraProjectionInClass n G C U x

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