Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.GroupLike
ProCGroups/FoxDifferential/Completed/DifferentialModule/Map/GroupLike

ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.GroupLike

1 Theorem

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraMap_of The completed prime-power group-algebra map sends the group-like element of g to the group-like element of ψ g.
import
Imported by

Declarations

Theorem FoxDifferential.primePowerCompletedGroupAlgebraMap_of 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraMap_of
    (ψ : ContinuousMonoidHom G H) (g : G) :
    primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
        (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := G) g) =
      primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := H) (ψ g)

The completed prime-power group-algebra map sends the group-like element of g to the group-like element of ψ g.

Show Lean proof