Def TannakaDuality.FiniteGroup.leftRegularFDRepHom

Modification history

2026-10-04 10:20
Mathlib/RepresentationTheory/Tannaka.lean
chore(CategoryTheory): `End` and `Aut` as `1`-field structures (#43759) …
Modified TannakaDuality.FiniteGroup.leftRegularFDRepHomView on Github →
2025-05-02 16:05
Mathlib/RepresentationTheory/Tannaka.lean
feat: Tannaka duality for finite groups (#22176) …
Added TannakaDuality.FiniteGroup.leftRegularFDRepHomView on Github →