Commit 2024-07-11 19:31 6ba2ff8f

View on Github →

chore(RepresentationTheory): rename FdRep to FDRep (#14309) As discussed on Zulip

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RepresentationTheory/Character.lean

added theorem FDRep.average_char_eq_finrank_invariants

added theorem FDRep.char_conj

added theorem FDRep.char_dual

added theorem FDRep.char_iso

added theorem FDRep.char_linHom

added theorem FDRep.char_mul_comm

added theorem FDRep.char_one

added theorem FDRep.char_orthonormal

added theorem FDRep.char_tensor'

added theorem FDRep.char_tensor

added def FDRep.character

deleted theorem FdRep.average_char_eq_finrank_invariants

deleted theorem FdRep.char_conj

deleted theorem FdRep.char_dual

deleted theorem FdRep.char_iso

deleted theorem FdRep.char_linHom

deleted theorem FdRep.char_mul_comm

deleted theorem FdRep.char_one

deleted theorem FdRep.char_orthonormal

deleted theorem FdRep.char_tensor'

deleted theorem FdRep.char_tensor

deleted def FdRep.character

Renamed Mathlib/RepresentationTheory/FdRep.lean to 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.ρ

deleted theorem FdRep.Iso.conj_ρ

deleted theorem FdRep.dualTensorIsoLinHom_hom_hom

deleted theorem FdRep.finrank_hom_simple_simple

deleted def FdRep.forget₂HomLinearEquiv

deleted theorem FdRep.forget₂_ρ

deleted def FdRep.isoToLinearEquiv

deleted def FdRep.of

deleted def FdRep.ρ

Modified Mathlib/RepresentationTheory/Invariants.lean

added def Representation.linHom.invariantsEquivFDRepHom

deleted def Representation.linHom.invariantsEquivFdRepHom

Modified docs/overview.yaml

Modified docs/undergrad.yaml