Commit 2023-07-01 20:46 b4a49ec9

View on Github →

feat: port RepresentationTheory.FdRep (#5612)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/FdRep.lean

added theorem FdRep.Iso.conj_ρ

added theorem FdRep.dualTensorIsoLinHom_hom_hom

added theorem FdRep.finrank_hom_simple_simple

added def FdRep.forget₂HomLinearEquiv

added theorem FdRep.forget₂_ρ

added def FdRep.isoToLinearEquiv

added def FdRep.of

added def FdRep.ρ