Module

MonoidHom_map_transfer_eq_transfer_comp.lean

Nyll.AlgebraicCurves.Foundations.Algebra.MonoidHom_map_transfer_eq_transfer_comp

1 declaration indexed from sourceView source ↗

Module documentation

Monoid Hom map transfer eq transfer comp

Imports2

Mathlib.GroupTheory.Transfer
Mathlib.GroupTheory.Abelianization.Defs

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

theorem

map_transfer_eq_transfer_comp

L25 ↗

MonoidHom.map_transfer_eq_transfer_comp

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MonoidHom_map_transfer_eq_transfer_comp

Lean source · statement

theorem _root_.MonoidHom.map_transfer_eq_transfer_comp
    {G : Type*} [Group G] {H : Subgroup G} [H.FiniteIndex]
    {A B : Type*} [CommGroup A] [CommGroup B] (ϕ : ↥H →* A) (f : A →* B) (g : G) :
    f (MonoidHom.transfer ϕ g) = MonoidHom.transfer (f.comp ϕ) g

Module documentation

Monoid Hom map transfer eq transfer comp

Declarations

map_transfer_eq_transfer_comp