Commit 2025-05-02 16:05 d516886e

View on Github →

feat: Tannaka duality for finite groups (#22176) Proves Tannaka duality for finite groups.

depends on: #23065

Estimated changes

Modified Mathlib/RepresentationTheory/Tannaka.lean

added def TannakaDuality.FiniteGroup.equiv

added theorem TannakaDuality.FiniteGroup.equivHom_surjective

added def TannakaDuality.FiniteGroup.leftRegularFDRepHom

added def TannakaDuality.FiniteGroup.ofRightFDRep

modified def TannakaDuality.FiniteGroup.rightFDRep

added def TannakaDuality.FiniteGroup.sumSMulInv

added theorem TannakaDuality.FiniteGroup.sumSMulInv_single_id

added theorem TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular

added theorem TannakaDuality.FiniteGroup.toRightFDRepComp_injective